Parser tweaks and fixes

- Completely remove the nexp = nexp syntax in favour of nexp == nexp. All our existing specs have already switched over. As part of this fix every test that used the old syntax, and update the generated aarch64 specs - Remove the `type when constraint` syntax. It just makes changing the parser in any way really awkward. - Change the syntax for declaring new types with multiple type parameters from: type foo('a : Type) ('n : Int), constraint = ... to type foo('a: Type, 'n: Int), constraint = ... This makes type declarations mimic function declarations, and makes the syntax for declaring types match the syntax for using types, as foo is used as foo(type, nexp). None of our specifications use types with multiple type parameters so this change doesn't actually break anything, other than some tests. The brackets around the type parameters are now mandatory. - Experiment with splitting Type/Order type parameters from Int type parameters in the parser. Currently in a type bar(x, y, z) all of x, y, and z could be either numeric expressions, orders, or types. This means that in the parser we are severely restricted in what we can parse in numeric expressions because everything has to be parseable as a type (atyp) - it also means we can't introduce boolean type variables/expressions or other minisail features (like removing ticks from type variables!) because we are heavily constrained by what we can parse unambigiously due to how these different type parameters can be mixed and interleaved. There is now experimental syntax: vector::<'o, 'a>('n) <--> vector('n, 'o, 'a) which splits the type argument list into two between Type/Order-polymorphic arguments and Int-polymorphic arguments. The exact choice of delimiters isn't set in stone - ::< and > match generics in Rust. The obvious choices of < and > / [ and ] are ambigious in various ways. Using this syntax right now triggers a warning. - Fix undefined behaviour in C compilation when concatenating a 0-length vector with a 64-length vector.
author: Alasdair Armstrong 2018-11-30 18:54:42 +0000
committer: Alasdair Armstrong 2018-11-30 19:13:39 +0000
commit: 0363a325ca6c498e086519c4ecaf1f51dbff7f64 (patch)
tree: bb40aa476726b365bed73c02f1184147eda394cf
parent: e25d469d7dfccc46db663ebcd4e00a5bfcac499a (diff)
26 files changed, 353 insertions, 320 deletions
diff --git a/aarch64/Makefile b/aarch64/Makefile
index 38900d5f..aa4d5301 100644
--- a/aarch64/Makefile
+++ b/aarch64/Makefile
@@ -13,6 +13,9 @@ aarch64_c: aarch64.c
 aarch64: no_vector.sail
 	$(SAIL) $^ -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
+
 aarch64.lem: no_vector.sail
 	$(SAIL) $^ -o aarch64 -lem -lem_lib Aarch64_extras -memo_z3 -undefined_gen -no_lexp_bounds_check
 aarch64_types.lem: aarch64.lem
diff --git a/aarch64/full/spec.sail b/aarch64/full/spec.sail
index 897fa56e..d98322fd 100644
--- a/aarch64/full/spec.sail
+++ b/aarch64/full/spec.sail
@@ -2006,7 +2006,7 @@ val BigEndianReverse : forall ('width : Int), 'width >= 0 & 'width >= 0.
 function BigEndianReverse value_name = {
   assert('width == 8 | 'width == 16 | 'width == 32 | 'width == 64 | 'width == 128);
   let 'half = 'width / 2;
-  assert(constraint('half * 2 = 'width));
+  assert(constraint('half * 2 == 'width));
   if 'width == 8 then return(value_name) else ();
   return(BigEndianReverse(slice(value_name, 0, half)) @ BigEndianReverse(slice(value_name, half, 'width - half)))
 }
@@ -2131,7 +2131,7 @@ val Replicate : forall ('M : Int) ('N : Int), 'M >= 0 & 'N >= 0.
 function Replicate x = {
   assert('N % 'M == 0, "((N MOD M) == 0)");
   let 'O = 'N / 'M;
-  assert(constraint('O * 'M = 'N));
+  assert(constraint('O * 'M == 'N));
   return(replicate_bits(x, 'N / 'M))
 }
 
@@ -2945,7 +2945,7 @@ val aarch64_integer_insext_insert_movewide : (int, int, bits(16), MoveWideOp, in
 
 function aarch64_integer_insext_insert_movewide ('d, 'datasize, imm, opcode, 'pos) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   result : bits('datasize) = undefined;
   if opcode == MoveWideOp_K then result = aget_X(d) else result = Zeros();
   result = __SetSlice_bits(datasize, 16, result, pos, imm);
@@ -2957,7 +2957,7 @@ val aarch64_integer_insext_extract_immediate : (int, int, int, int, int) -> unit
 
 function aarch64_integer_insext_extract_immediate ('d, 'datasize, 'lsb, 'm, 'n) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   result : bits('datasize) = undefined;
   operand1 : bits('datasize) = aget_X(n);
   operand2 : bits('datasize) = aget_X(m);
@@ -2970,7 +2970,7 @@ val aarch64_integer_arithmetic_rev : (int, int, int, int) -> unit effect {escape
 
 function aarch64_integer_arithmetic_rev ('container_size, 'd, 'datasize, 'n) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   operand : bits('datasize) = aget_X(n);
   result : bits('datasize) = undefined;
   containers : int = datasize / container_size;
@@ -2992,7 +2992,7 @@ val aarch64_integer_arithmetic_rbit : (int, int, int) -> unit effect {escape, rr
 
 function aarch64_integer_arithmetic_rbit ('d, 'datasize, 'n) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   operand : bits('datasize) = aget_X(n);
   result : bits('datasize) = undefined;
   foreach (i from 0 to (datasize - 1) by 1 in inc)
@@ -3014,7 +3014,7 @@ val aarch64_integer_arithmetic_mul_widening_64128hi : (int, int, int, int, bool)
 
 function aarch64_integer_arithmetic_mul_widening_64128hi ('d, 'datasize, 'm, 'n, unsigned) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   operand1 : bits('datasize) = aget_X(n);
   operand2 : bits('datasize) = aget_X(m);
   result : int = asl_Int(operand1, unsigned) * asl_Int(operand2, unsigned);
@@ -3041,7 +3041,7 @@ function aarch64_integer_arithmetic_mul_widening_3264 ('a, 'd, 'datasize, 'dests
   assert(constraint('destsize in {32, 64}), "destsize constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   operand1 : bits('datasize) = aget_X(n);
   operand2 : bits('datasize) = aget_X(m);
   operand3 : bits('destsize) = aget_X(a);
@@ -3071,7 +3071,7 @@ function aarch64_integer_arithmetic_mul_uniform_addsub ('a, 'd, 'datasize, 'dest
   assert(constraint('destsize in {32, 64}), "destsize constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   operand1 : bits('datasize) = aget_X(n);
   operand2 : bits('datasize) = aget_X(m);
   operand3 : bits('destsize) = aget_X(a);
@@ -3098,7 +3098,7 @@ val aarch64_integer_arithmetic_div : (int, int, int, int, bool) -> unit effect {
 
 function aarch64_integer_arithmetic_div ('d, 'datasize, 'm, 'n, unsigned) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   operand1 : bits('datasize) = aget_X(n);
   operand2 : bits('datasize) = aget_X(m);
   result : int = undefined;
@@ -3122,7 +3122,7 @@ val aarch64_integer_arithmetic_cnt : (int, int, int, CountOp) -> unit effect {es
 
 function aarch64_integer_arithmetic_cnt ('d, 'datasize, 'n, opcode) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   result : int = undefined;
   operand1 : bits('datasize) = aget_X(n);
   if opcode == CountOp_CLZ then result = CountLeadingZeroBits(operand1) else result = CountLeadingSignBits(operand1);
@@ -3144,7 +3144,7 @@ val aarch64_integer_arithmetic_addsub_carry : (int, int, int, int, bool, bool) -
 
 function aarch64_integer_arithmetic_addsub_carry ('d, 'datasize, 'm, 'n, setflags, sub_op) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   result : bits('datasize) = undefined;
   operand1 : bits('datasize) = aget_X(n);
   operand2 : bits('datasize) = aget_X(m);
@@ -3341,7 +3341,7 @@ val aarch64_integer_bitfield : forall ('datasize : Int).
 
 function aarch64_integer_bitfield ('R, 'S, 'd, datasize, extend, inzero, 'n, tmask, wmask) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   dst : bits('datasize) = if inzero then Zeros() else aget_X(d);
   src : bits('datasize) = aget_X(n);
   bot : bits('datasize) = dst & ~(wmask) | ROR(src, R) & wmask;
@@ -3367,7 +3367,7 @@ val aarch64_integer_shift_variable : (int, int, int, int, ShiftType) -> unit eff
 
 function aarch64_integer_shift_variable ('d, 'datasize, 'm, 'n, shift_type) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   result : bits('datasize) = undefined;
   operand2 : bits('datasize) = aget_X(m);
   result = ShiftReg(n, shift_type, UInt(operand2) % datasize);
@@ -3390,7 +3390,7 @@ val aarch64_integer_logical_shiftedreg : (int, int, bool, int, int, LogicalOp, b
 
 function aarch64_integer_logical_shiftedreg ('d, 'datasize, invert, 'm, 'n, op, setflags, 'shift_amount, shift_type) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   operand1 : bits('datasize) = aget_X(n);
   operand2 : bits('datasize) = ShiftReg(m, shift_type, shift_amount);
   if invert then operand2 = ~(operand2) else ();
@@ -3408,7 +3408,7 @@ val aarch64_integer_arithmetic_addsub_shiftedreg : (int, int, int, int, bool, in
 
 function aarch64_integer_arithmetic_addsub_shiftedreg ('d, 'datasize, 'm, 'n, setflags, 'shift_amount, shift_type, sub_op) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   result : bits('datasize) = undefined;
   operand1 : bits('datasize) = aget_X(n);
   operand2 : bits('datasize) = ShiftReg(m, shift_type, shift_amount);
@@ -3764,7 +3764,7 @@ val aarch64_integer_logical_immediate : forall ('datasize : Int).
 
 function aarch64_integer_logical_immediate ('d, datasize, imm, 'n, op, setflags) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   result : bits('datasize) = undefined;
   operand1 : bits('datasize) = aget_X(n);
   operand2 : bits('datasize) = imm;
@@ -3782,7 +3782,7 @@ val aarch64_integer_arithmetic_addsub_immediate : forall ('datasize : Int).
 
 function aarch64_integer_arithmetic_addsub_immediate ('d, datasize, imm, 'n, setflags, sub_op) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   result : bits('datasize) = undefined;
   operand1 : bits('datasize) = if n == 31 then aget_SP() else aget_X(n);
   operand2 : bits('datasize) = imm;
@@ -3801,7 +3801,7 @@ val aarch64_integer_arithmetic_addsub_extendedreg : (int, int, ExtendType, int,
 
 function aarch64_integer_arithmetic_addsub_extendedreg ('d, 'datasize, extend_type, 'm, 'n, setflags, 'shift, sub_op) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   result : bits('datasize) = undefined;
   operand1 : bits('datasize) = if n == 31 then aget_SP() else aget_X(n);
   operand2 : bits('datasize) = ExtendReg(m, extend_type, shift);
@@ -5319,7 +5319,7 @@ function Reduce (op, input, esize) = {
   result : bits('esize) = undefined;
   if 'N == 'esize then return(input) else ();
   let 'half = 'N / 2;
-  assert(constraint('half * 2 = 'N));
+  assert(constraint('half * 2 == 'N));
   hi = Reduce(op, slice(input, half, negate(half) + 'N), 'esize);
   lo = Reduce(op, slice(input, 0, half), 'esize);
   match op {
@@ -5821,7 +5821,7 @@ val aarch64_integer_conditional_select : (bits(4), int, int, bool, bool, int, in
 
 function aarch64_integer_conditional_select (condition, 'd, 'datasize, else_inc, else_inv, 'm, 'n) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   result : bits('datasize) = undefined;
   operand1 : bits('datasize) = aget_X(n);
   operand2 : bits('datasize) = aget_X(m);
@@ -5851,7 +5851,7 @@ val aarch64_integer_conditional_compare_register : (bits(4), int, bits(4), int,
 
 function aarch64_integer_conditional_compare_register (condition, 'datasize, flags__arg, 'm, 'n, sub_op) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   flags = flags__arg;
   operand1 : bits('datasize) = aget_X(n);
   operand2 : bits('datasize) = aget_X(m);
@@ -5885,7 +5885,7 @@ val aarch64_integer_conditional_compare_immediate : forall ('datasize : Int).
 
 function aarch64_integer_conditional_compare_immediate (condition, datasize, flags__arg, imm, 'n, sub_op) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   flags = flags__arg;
   operand1 : bits('datasize) = aget_X(n);
   operand2 : bits('datasize) = imm;
@@ -7856,7 +7856,7 @@ val aarch64_branch_conditional_test : (int, bits(1), int, bits(64), int) -> unit
 
 function aarch64_branch_conditional_test ('bit_pos, bit_val, 'datasize, offset, 't) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   operand : bits('datasize) = aget_X(t);
   if [operand[bit_pos]] == bit_val then BranchTo(aget_PC() + offset, BranchType_JMP) else ()
 }
@@ -7890,7 +7890,7 @@ val aarch64_branch_conditional_compare : (int, bool, bits(64), int) -> unit effe
 
 function aarch64_branch_conditional_compare ('datasize, iszero, offset, 't) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   operand1 : bits('datasize) = aget_X(t);
   if IsZero(operand1) == iszero then BranchTo(aget_PC() + offset, BranchType_JMP) else ()
 }
@@ -8998,7 +8998,7 @@ val aarch64_vector_transfer_vector_table : (int, int, int, bool, int, int, int)
 
 function aarch64_vector_transfer_vector_table ('d, 'datasize, 'elements, is_tbl, 'm, n__arg, 'regs) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   assert(constraint('regs >= 1 & 'elements >= 1));
   n : int = n__arg;
   CheckFPAdvSIMDEnabled64();
@@ -9041,7 +9041,7 @@ function aarch64_vector_transfer_vector_permute_zip ('d, 'datasize, 'esize, 'm,
   assert(constraint('esize >= 0), "esize constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand1 : bits('datasize) = aget_V(n);
   operand2 : bits('datasize) = aget_V(m);
@@ -9062,7 +9062,7 @@ function aarch64_vector_transfer_vector_permute_unzip ('d, 'datasize, 'elements,
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operandl : bits('datasize) = aget_V(n);
   operandh : bits('datasize) = aget_V(m);
@@ -9080,7 +9080,7 @@ function aarch64_vector_transfer_vector_permute_transpose ('d, 'datasize, 'esize
   assert(constraint('esize >= 0), "esize constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand1 : bits('datasize) = aget_V(n);
   operand2 : bits('datasize) = aget_V(m);
@@ -9109,7 +9109,7 @@ val aarch64_vector_transfer_vector_extract : (int, int, int, int, int) -> unit e
 
 function aarch64_vector_transfer_vector_extract ('d, 'datasize, 'm, 'n, 'position) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   hi : bits('datasize) = aget_V(m);
   lo : bits('datasize) = aget_V(n);
@@ -9125,7 +9125,7 @@ function aarch64_vector_transfer_vector_cpydup_sisd ('d, 'datasize, 'elements, '
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand : bits('idxdsize) = aget_V(n);
   result : bits('datasize) = undefined;
@@ -9142,7 +9142,7 @@ function aarch64_vector_transfer_integer_move_unsigned ('d, 'datasize, 'esize, '
   assert(constraint('esize >= 0), "esize constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand : bits('idxdsize) = aget_V(n);
   aset_X(d, ZeroExtend(aget_Elem(operand, index, esize), datasize))
@@ -9155,7 +9155,7 @@ function aarch64_vector_transfer_integer_move_signed ('d, 'datasize, 'esize, 'id
   assert(constraint('esize >= 0), "esize constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand : bits('idxdsize) = aget_V(n);
   aset_X(d, SignExtend(aget_Elem(operand, index, esize), datasize))
@@ -9167,7 +9167,7 @@ function aarch64_vector_transfer_integer_insert ('d, 'datasize, 'esize, 'index,
   assert(constraint('esize >= 0), "esize constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   element : bits('esize) = aget_X(n);
   result : bits('datasize) = aget_V(d);
@@ -9182,7 +9182,7 @@ function aarch64_vector_transfer_integer_dup ('d, 'datasize, 'elements, 'esize,
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   element : bits('esize) = aget_X(n);
   result : bits('datasize) = undefined;
@@ -9198,7 +9198,7 @@ function aarch64_vector_shift_right_sisd (accumulate, 'd, 'datasize, 'elements,
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand : bits('datasize) = aget_V(n);
   operand2 : bits('datasize) = undefined;
@@ -9220,7 +9220,7 @@ function aarch64_vector_shift_rightnarrow_uniform_sisd ('d, 'datasize, 'elements
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand : bits(2 * 'datasize) = aget_V(n);
   result : bits('datasize) = undefined;
@@ -9244,7 +9244,7 @@ function aarch64_vector_shift_rightnarrow_nonuniform_sisd ('d, 'datasize, 'eleme
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand : bits(2 * 'datasize) = aget_V(n);
   result : bits('datasize) = undefined;
@@ -9268,7 +9268,7 @@ function aarch64_vector_shift_rightnarrow_logical ('d, 'datasize, 'elements, 'es
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand : bits(2 * 'datasize) = aget_V(n);
   result : bits('datasize) = undefined;
@@ -9288,7 +9288,7 @@ function aarch64_vector_shift_rightinsert_sisd ('d, 'datasize, 'elements, 'esize
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand : bits('datasize) = aget_V(n);
   operand2 : bits('datasize) = aget_V(d);
@@ -9309,7 +9309,7 @@ function aarch64_vector_shift_left_sisd ('d, 'datasize, 'elements, 'esize, 'n, '
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand : bits('datasize) = aget_V(n);
   result : bits('datasize) = undefined;
@@ -9325,7 +9325,7 @@ function aarch64_vector_shift_leftsat_sisd ('d, 'datasize, dst_unsigned, 'elemen
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand : bits('datasize) = aget_V(n);
   result : bits('datasize) = undefined;
@@ -9348,7 +9348,7 @@ function aarch64_vector_shift_leftlong ('d, 'datasize, 'elements, 'esize, 'n, 'p
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand : bits('datasize) = aget_Vpart(n, part);
   result : bits(2 * 'datasize) = undefined;
@@ -9367,7 +9367,7 @@ function aarch64_vector_shift_leftinsert_sisd ('d, 'datasize, 'elements, 'esize,
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand : bits('datasize) = aget_V(n);
   operand2 : bits('datasize) = aget_V(d);
@@ -9388,7 +9388,7 @@ function aarch64_vector_shift_conv_int_sisd ('d, 'datasize, 'elements, 'esize, '
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand : bits('datasize) = aget_V(n);
   result : bits('datasize) = undefined;
@@ -9407,7 +9407,7 @@ function aarch64_vector_shift_conv_float_sisd ('d, 'datasize, 'elements, 'esize,
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand : bits('datasize) = aget_V(n);
   result : bits('datasize) = undefined;
@@ -9426,7 +9426,7 @@ function aarch64_vector_reduce_intmax ('d, 'datasize, 'elements, 'esize, min, 'n
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand : bits('datasize) = aget_V(n);
   maxmin : int = undefined;
@@ -9445,7 +9445,7 @@ function aarch64_vector_reduce_fp16maxnm_sisd ('d, 'datasize, 'esize, 'n, op) =
   assert(constraint('esize >= 0), "esize constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand : bits('datasize) = aget_V(n);
   aset_V(d, Reduce(op, operand, esize))
@@ -9470,7 +9470,7 @@ function aarch64_vector_reduce_fp16maxnm_simd ('d, 'datasize, 'esize, 'n, op) =
   assert(constraint('esize >= 0), "esize constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand : bits('datasize) = aget_V(n);
   aset_V(d, Reduce(op, operand, esize))
@@ -9482,7 +9482,7 @@ function aarch64_vector_reduce_fp16max_sisd ('d, 'datasize, 'esize, 'n, op) = {
   assert(constraint('esize >= 0), "esize constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand : bits('datasize) = aget_V(n);
   aset_V(d, Reduce(op, operand, esize))
@@ -9507,7 +9507,7 @@ function aarch64_vector_reduce_fp16max_simd ('d, 'datasize, 'esize, 'n, op) = {
   assert(constraint('esize >= 0), "esize constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand : bits('datasize) = aget_V(n);
   aset_V(d, Reduce(op, operand, esize))
@@ -9519,7 +9519,7 @@ function aarch64_vector_reduce_fp16add_sisd ('d, 'datasize, 'esize, 'n, op) = {
   assert(constraint('esize >= 0), "esize constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand : bits('datasize) = aget_V(n);
   aset_V(d, Reduce(op, operand, esize))
@@ -9544,7 +9544,7 @@ function aarch64_vector_reduce_add_sisd ('d, 'datasize, 'esize, 'n, op) = {
   assert(constraint('esize >= 0), "esize constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand : bits('datasize) = aget_V(n);
   aset_V(d, Reduce(op, operand, esize))
@@ -9556,7 +9556,7 @@ function aarch64_vector_reduce_add_simd ('d, 'datasize, 'esize, 'n, op) = {
   assert(constraint('esize >= 0), "esize constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand : bits('datasize) = aget_V(n);
   aset_V(d, Reduce(op, operand, esize))
@@ -9569,7 +9569,7 @@ function aarch64_vector_reduce_addlong ('d, 'datasize, 'elements, 'esize, 'n, un
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand : bits('datasize) = aget_V(n);
   sum : int = asl_Int(aget_Elem(operand, 0, esize), unsigned);
@@ -9583,7 +9583,7 @@ val aarch64_vector_logical : forall ('datasize : Int).
 
 function aarch64_vector_logical (datasize, imm, operation, 'rd) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand : bits('datasize) = undefined;
   result : bits('datasize) = undefined;
@@ -9607,7 +9607,7 @@ val aarch64_vector_fp16_movi : forall ('datasize : Int).
 
 function aarch64_vector_fp16_movi (datasize, imm, 'rd) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   aset_V(rd, imm)
 }
@@ -9619,7 +9619,7 @@ function aarch64_vector_arithmetic_unary_special_sqrtfp16 ('d, 'datasize, 'eleme
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand : bits('datasize) = aget_V(n);
   result : bits('datasize) = undefined;
@@ -9637,7 +9637,7 @@ function aarch64_vector_arithmetic_unary_special_sqrtest_int ('d, 'datasize, 'el
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand : bits('datasize) = aget_V(n);
   result : bits('datasize) = undefined;
@@ -9656,7 +9656,7 @@ function aarch64_vector_arithmetic_unary_special_sqrtest_fp16_sisd ('d, 'datasiz
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand : bits('datasize) = aget_V(n);
   result : bits('datasize) = undefined;
@@ -9686,7 +9686,7 @@ function aarch64_vector_arithmetic_unary_special_recip_int ('d, 'datasize, 'elem
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand : bits('datasize) = aget_V(n);
   result : bits('datasize) = undefined;
@@ -9705,7 +9705,7 @@ function aarch64_vector_arithmetic_unary_special_recip_fp16_sisd ('d, 'datasize,
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand : bits('datasize) = aget_V(n);
   result : bits('datasize) = undefined;
@@ -9736,7 +9736,7 @@ function aarch64_vector_arithmetic_unary_special_frecpxfp16 ('d, 'datasize, 'ele
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand : bits('datasize) = aget_V(n);
   result : bits('datasize) = undefined;
@@ -9767,7 +9767,7 @@ function aarch64_vector_arithmetic_unary_shift ('d, 'datasize, 'elements, 'esize
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand : bits('datasize) = aget_Vpart(n, part);
   result : bits(2 * 'datasize) = undefined;
@@ -9785,7 +9785,7 @@ function aarch64_vector_arithmetic_unary_rev ('containers, 'd, 'datasize, 'eleme
   assert(constraint('esize >= 0), "esize constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand : bits('datasize) = aget_V(n);
   result : bits('datasize) = undefined;
@@ -9809,7 +9809,7 @@ function aarch64_vector_arithmetic_unary_rbit ('d, 'datasize, 'elements, 'esize,
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand : bits('datasize) = aget_V(n);
   result : bits('datasize) = undefined;
@@ -9843,7 +9843,7 @@ function aarch64_vector_arithmetic_unary_not ('d, 'datasize, 'elements, 'esize,
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand : bits('datasize) = aget_V(n);
   result : bits('datasize) = undefined;
@@ -9874,7 +9874,7 @@ function aarch64_vector_arithmetic_unary_fp16_round ('d, 'datasize, 'elements, '
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand : bits('datasize) = aget_V(n);
   result : bits('datasize) = undefined;
@@ -9893,7 +9893,7 @@ function aarch64_vector_arithmetic_unary_fp16_conv_int_sisd ('d, 'datasize, 'ele
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand : bits('datasize) = aget_V(n);
   result : bits('datasize) = undefined;
@@ -9926,7 +9926,7 @@ function aarch64_vector_arithmetic_unary_fp16_conv_float_tieaway_sisd ('d, 'data
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand : bits('datasize) = aget_V(n);
   result : bits('datasize) = undefined;
@@ -9959,7 +9959,7 @@ function aarch64_vector_arithmetic_unary_fp16_conv_float_bulk_sisd ('d, 'datasiz
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand : bits('datasize) = aget_V(n);
   result : bits('datasize) = undefined;
@@ -9992,7 +9992,7 @@ function aarch64_vector_arithmetic_unary_float_xtn_sisd ('d, 'datasize, 'element
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand : bits(2 * 'datasize) = aget_V(n);
   result : bits('datasize) = undefined;
@@ -10008,7 +10008,7 @@ function aarch64_vector_arithmetic_unary_float_widen ('d, 'datasize, 'elements,
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand : bits('datasize) = aget_Vpart(n, part);
   result : bits(2 * 'datasize) = undefined;
@@ -10037,7 +10037,7 @@ function aarch64_vector_arithmetic_unary_float_narrow ('d, 'datasize, 'elements,
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand : bits(2 * 'datasize) = aget_V(n);
   result : bits('datasize) = undefined;
@@ -10066,7 +10066,7 @@ function aarch64_vector_arithmetic_unary_extract_sqxtun_sisd ('d, 'datasize, 'el
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand : bits(2 * 'datasize) = aget_V(n);
   result : bits('datasize) = undefined;
@@ -10089,7 +10089,7 @@ function aarch64_vector_arithmetic_unary_extract_sat_sisd ('d, 'datasize, 'eleme
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand : bits(2 * 'datasize) = aget_V(n);
   result : bits('datasize) = undefined;
@@ -10112,7 +10112,7 @@ function aarch64_vector_arithmetic_unary_extract_nosat ('d, 'datasize, 'elements
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand : bits(2 * 'datasize) = aget_V(n);
   result : bits('datasize) = undefined;
@@ -10131,7 +10131,7 @@ function aarch64_vector_arithmetic_unary_diffneg_sat_sisd ('d, 'datasize, 'eleme
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand : bits('datasize) = aget_V(n);
   result : bits('datasize) = undefined;
@@ -10168,7 +10168,7 @@ function aarch64_vector_arithmetic_unary_diffneg_int_sisd ('d, 'datasize, 'eleme
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand : bits('datasize) = aget_V(n);
   result : bits('datasize) = undefined;
@@ -10188,7 +10188,7 @@ function aarch64_vector_arithmetic_unary_diffneg_fp16 ('d, 'datasize, 'elements,
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand : bits('datasize) = aget_V(n);
   result : bits('datasize) = undefined;
@@ -10205,7 +10205,7 @@ val aarch64_vector_arithmetic_unary_cnt : (int, int, int, int, int) -> unit effe
 
 function aarch64_vector_arithmetic_unary_cnt ('d, 'datasize, 'elements, 'esize, 'n) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   assert('elements >= 1 & 'esize >= 1);
   CheckFPAdvSIMDEnabled64();
   operand : bits('datasize) = aget_V(n);
@@ -10225,7 +10225,7 @@ function aarch64_vector_arithmetic_unary_cmp_int_lessthan_sisd (comparison, 'd,
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand : bits('datasize) = aget_V(n);
   result : bits('datasize) = undefined;
@@ -10252,7 +10252,7 @@ function aarch64_vector_arithmetic_unary_cmp_int_bulk_sisd (comparison, 'd, 'dat
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand : bits('datasize) = aget_V(n);
   result : bits('datasize) = undefined;
@@ -10279,7 +10279,7 @@ function aarch64_vector_arithmetic_unary_cmp_fp16_lessthan_sisd (comparison, 'd,
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand : bits('datasize) = aget_V(n);
   result : bits('datasize) = undefined;
@@ -10320,7 +10320,7 @@ function aarch64_vector_arithmetic_unary_cmp_fp16_bulk_sisd (comparison, 'd, 'da
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand : bits('datasize) = aget_V(n);
   result : bits('datasize) = undefined;
@@ -10364,7 +10364,7 @@ val aarch64_vector_arithmetic_unary_clsz : (CountOp, int, int, int, int, int) ->
 
 function aarch64_vector_arithmetic_unary_clsz (countop, 'd, 'datasize, 'elements, 'esize, 'n) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   assert('elements >= 1 & 'esize >= 3);
   CheckFPAdvSIMDEnabled64();
   operand : bits('datasize) = aget_V(n);
@@ -10386,7 +10386,7 @@ function aarch64_vector_arithmetic_unary_add_saturating_sisd ('d, 'datasize, 'el
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand : bits('datasize) = aget_V(n);
   result : bits('datasize) = undefined;
@@ -10425,7 +10425,7 @@ function aarch64_vector_arithmetic_unary_add_pairwise (acc, 'd, 'datasize, 'elem
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand : bits('datasize) = aget_V(n);
   result : bits('datasize) = undefined;
@@ -10449,7 +10449,7 @@ function aarch64_vector_arithmetic_binary_uniform_sub_saturating_sisd ('d, 'data
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand1 : bits('datasize) = aget_V(n);
   operand2 : bits('datasize) = aget_V(m);
@@ -10491,7 +10491,7 @@ function aarch64_vector_arithmetic_binary_uniform_sub_int ('d, 'datasize, 'eleme
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand1 : bits('datasize) = aget_V(n);
   operand2 : bits('datasize) = aget_V(m);
@@ -10515,7 +10515,7 @@ function aarch64_vector_arithmetic_binary_uniform_sub_fp16_sisd (abs, 'd, 'datas
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand1 : bits('datasize) = aget_V(n);
   operand2 : bits('datasize) = aget_V(m);
@@ -10553,7 +10553,7 @@ function aarch64_vector_arithmetic_binary_uniform_sub_fp16_simd (abs, 'd, 'datas
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand1 : bits('datasize) = aget_V(n);
   operand2 : bits('datasize) = aget_V(m);
@@ -10577,7 +10577,7 @@ function aarch64_vector_arithmetic_binary_uniform_shift_sisd ('d, 'datasize, 'el
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand1 : bits('datasize) = aget_V(n);
   operand2 : bits('datasize) = aget_V(m);
@@ -10607,7 +10607,7 @@ function aarch64_vector_arithmetic_binary_uniform_rsqrtsfp16_sisd ('d, 'datasize
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand1 : bits('datasize) = aget_V(n);
   operand2 : bits('datasize) = aget_V(m);
@@ -10642,7 +10642,7 @@ function aarch64_vector_arithmetic_binary_uniform_recpsfp16_sisd ('d, 'datasize,
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand1 : bits('datasize) = aget_V(n);
   operand2 : bits('datasize) = aget_V(m);
@@ -10674,7 +10674,7 @@ val aarch64_vector_arithmetic_binary_uniform_mul_int_product : (int, int, int, i
 
 function aarch64_vector_arithmetic_binary_uniform_mul_int_product ('d, 'datasize, 'elements, 'esize, 'm, 'n, poly) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   assert('elements >= 1 & 'esize >= 1);
   CheckFPAdvSIMDEnabled64();
   operand1 : bits('datasize) = aget_V(n);
@@ -10700,7 +10700,7 @@ function aarch64_vector_arithmetic_binary_uniform_mul_int_doubling_sisd ('d, 'da
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand1 : bits('datasize) = aget_V(n);
   operand2 : bits('datasize) = aget_V(m);
@@ -10729,7 +10729,7 @@ function aarch64_vector_arithmetic_binary_uniform_mul_int_doubling_accum_sisd ('
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand1 : bits('datasize) = aget_V(n);
   operand2 : bits('datasize) = aget_V(m);
@@ -10762,7 +10762,7 @@ function aarch64_vector_arithmetic_binary_uniform_mul_int_dotp ('d, 'datasize, '
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand1 : bits('datasize) = aget_V(n);
   operand2 : bits('datasize) = aget_V(m);
@@ -10793,7 +10793,7 @@ function aarch64_vector_arithmetic_binary_uniform_mul_int_accum ('d, 'datasize,
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand1 : bits('datasize) = aget_V(n);
   operand2 : bits('datasize) = aget_V(m);
@@ -10818,7 +10818,7 @@ function aarch64_vector_arithmetic_binary_uniform_mul_fp16_product ('d, 'datasiz
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand1 : bits('datasize) = aget_V(n);
   operand2 : bits('datasize) = aget_V(m);
@@ -10840,7 +10840,7 @@ function aarch64_vector_arithmetic_binary_uniform_mul_fp16_fused ('d, 'datasize,
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand1 : bits('datasize) = aget_V(n);
   operand2 : bits('datasize) = aget_V(m);
@@ -10864,7 +10864,7 @@ function aarch64_vector_arithmetic_binary_uniform_mul_fp16_extended_sisd ('d, 'd
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand1 : bits('datasize) = aget_V(n);
   operand2 : bits('datasize) = aget_V(m);
@@ -10899,7 +10899,7 @@ function aarch64_vector_arithmetic_binary_uniform_mul_fp_complex ('d, 'datasize,
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand1 : bits('datasize) = aget_V(n);
   operand2 : bits('datasize) = aget_V(m);
@@ -10949,7 +10949,7 @@ function aarch64_vector_arithmetic_binary_uniform_maxmin_single ('d, 'datasize,
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand1 : bits('datasize) = aget_V(n);
   operand2 : bits('datasize) = aget_V(m);
@@ -10973,7 +10973,7 @@ function aarch64_vector_arithmetic_binary_uniform_maxmin_pair ('d, 'datasize, 'e
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand1 : bits('datasize) = aget_V(n);
   operand2 : bits('datasize) = aget_V(m);
@@ -10998,7 +10998,7 @@ function aarch64_vector_arithmetic_binary_uniform_maxmin_fp16_2008 ('d, 'datasiz
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand1 : bits('datasize) = aget_V(n);
   operand2 : bits('datasize) = aget_V(m);
@@ -11026,7 +11026,7 @@ function aarch64_vector_arithmetic_binary_uniform_maxmin_fp16_1985 ('d, 'datasiz
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand1 : bits('datasize) = aget_V(n);
   operand2 : bits('datasize) = aget_V(m);
@@ -11051,7 +11051,7 @@ val aarch64_vector_arithmetic_binary_uniform_logical_bsleor : (int, int, int, in
 
 function aarch64_vector_arithmetic_binary_uniform_logical_bsleor ('d, 'datasize, 'm, 'n, op) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand1 : bits('datasize) = undefined;
   operand2 : bits('datasize) = undefined;
@@ -11106,7 +11106,7 @@ val aarch64_vector_arithmetic_binary_uniform_logical_andorr : (int, int, bool, i
 
 function aarch64_vector_arithmetic_binary_uniform_logical_andorr ('d, 'datasize, invert, 'm, 'n, op) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand1 : bits('datasize) = aget_V(n);
   operand2 : bits('datasize) = aget_V(m);
@@ -11141,7 +11141,7 @@ function aarch64_vector_arithmetic_binary_uniform_divfp16 ('d, 'datasize, 'eleme
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand1 : bits('datasize) = aget_V(n);
   operand2 : bits('datasize) = aget_V(m);
@@ -11163,7 +11163,7 @@ function aarch64_vector_arithmetic_binary_uniform_diff (accumulate, 'd, 'datasiz
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand1 : bits('datasize) = aget_V(n);
   operand2 : bits('datasize) = aget_V(m);
@@ -11188,7 +11188,7 @@ function aarch64_vector_arithmetic_binary_uniform_cmp_int_sisd (cmp_eq, 'd, 'dat
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand1 : bits('datasize) = aget_V(n);
   operand2 : bits('datasize) = aget_V(m);
@@ -11212,7 +11212,7 @@ function aarch64_vector_arithmetic_binary_uniform_cmp_fp16_sisd (abs, cmp, 'd, '
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand1 : bits('datasize) = aget_V(n);
   operand2 : bits('datasize) = aget_V(m);
@@ -11244,7 +11244,7 @@ function aarch64_vector_arithmetic_binary_uniform_cmp_bitwise_sisd (and_test, 'd
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand1 : bits('datasize) = aget_V(n);
   operand2 : bits('datasize) = aget_V(m);
@@ -11268,7 +11268,7 @@ function aarch64_vector_arithmetic_binary_uniform_add_wrapping_single_sisd ('d,
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand1 : bits('datasize) = aget_V(n);
   operand2 : bits('datasize) = aget_V(m);
@@ -11290,7 +11290,7 @@ function aarch64_vector_arithmetic_binary_uniform_add_wrapping_pair ('d, 'datasi
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand1 : bits('datasize) = aget_V(n);
   operand2 : bits('datasize) = aget_V(m);
@@ -11313,7 +11313,7 @@ function aarch64_vector_arithmetic_binary_uniform_add_saturating_sisd ('d, 'data
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand1 : bits('datasize) = aget_V(n);
   operand2 : bits('datasize) = aget_V(m);
@@ -11355,7 +11355,7 @@ function aarch64_vector_arithmetic_binary_uniform_add_halving_truncating ('d, 'd
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand1 : bits('datasize) = aget_V(n);
   operand2 : bits('datasize) = aget_V(m);
@@ -11379,7 +11379,7 @@ function aarch64_vector_arithmetic_binary_uniform_add_halving_rounding ('d, 'dat
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand1 : bits('datasize) = aget_V(n);
   operand2 : bits('datasize) = aget_V(m);
@@ -11401,7 +11401,7 @@ function aarch64_vector_arithmetic_binary_uniform_add_fp16 ('d, 'datasize, 'elem
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand1 : bits('datasize) = aget_V(n);
   operand2 : bits('datasize) = aget_V(m);
@@ -11429,7 +11429,7 @@ function aarch64_vector_arithmetic_binary_uniform_add_fp_complex ('d, 'datasize,
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand1 : bits('datasize) = aget_V(n);
   operand2 : bits('datasize) = aget_V(m);
@@ -11462,7 +11462,7 @@ function aarch64_vector_arithmetic_binary_element_mul_long ('d, 'datasize, 'elem
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand1 : bits('datasize) = aget_Vpart(n, part);
   operand2 : bits('idxdsize) = aget_V(m);
@@ -11487,7 +11487,7 @@ function aarch64_vector_arithmetic_binary_element_mul_int ('d, 'datasize, 'eleme
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand1 : bits('datasize) = aget_V(n);
   operand2 : bits('idxdsize) = aget_V(m);
@@ -11512,7 +11512,7 @@ function aarch64_vector_arithmetic_binary_element_mul_high_sisd ('d, 'datasize,
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand1 : bits('datasize) = aget_V(n);
   operand2 : bits('idxdsize) = aget_V(m);
@@ -11542,7 +11542,7 @@ function aarch64_vector_arithmetic_binary_element_mul_fp16_sisd ('d, 'datasize,
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand1 : bits('datasize) = aget_V(n);
   operand2 : bits('idxdsize) = aget_V(m);
@@ -11564,7 +11564,7 @@ function aarch64_vector_arithmetic_binary_element_mul_double_sisd ('d, 'datasize
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand1 : bits('datasize) = aget_Vpart(n, part);
   operand2 : bits('idxdsize) = aget_V(m);
@@ -11591,7 +11591,7 @@ function aarch64_vector_arithmetic_binary_element_mulacc_long ('d, 'datasize, 'e
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand1 : bits('datasize) = aget_Vpart(n, part);
   operand2 : bits('idxdsize) = aget_V(m);
@@ -11617,7 +11617,7 @@ function aarch64_vector_arithmetic_binary_element_mulacc_int ('d, 'datasize, 'el
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand1 : bits('datasize) = aget_V(n);
   operand2 : bits('idxdsize) = aget_V(m);
@@ -11643,7 +11643,7 @@ function aarch64_vector_arithmetic_binary_element_mulacc_high_sisd ('d, 'datasiz
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand1 : bits('datasize) = aget_V(n);
   operand2 : bits('idxdsize) = aget_V(m);
@@ -11677,7 +11677,7 @@ function aarch64_vector_arithmetic_binary_element_mulacc_fp16_sisd ('d, 'datasiz
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand1 : bits('datasize) = aget_V(n);
   operand2 : bits('idxdsize) = aget_V(m);
@@ -11701,7 +11701,7 @@ function aarch64_vector_arithmetic_binary_element_mulacc_double_sisd ('d, 'datas
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand1 : bits('datasize) = aget_Vpart(n, part);
   operand2 : bits('idxdsize) = aget_V(m);
@@ -11733,7 +11733,7 @@ function aarch64_vector_arithmetic_binary_element_mulacc_complex ('d, 'datasize,
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand1 : bits('datasize) = aget_V(m);
   operand2 : bits('datasize) = aget_V(n);
@@ -11783,7 +11783,7 @@ function aarch64_vector_arithmetic_binary_element_dotp ('d, 'datasize, 'elements
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand1 : bits('datasize) = aget_V(n);
   operand2 : bits(128) = aget_V(m);
@@ -11814,7 +11814,7 @@ function aarch64_vector_arithmetic_binary_disparate_mul_product ('d, 'datasize,
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand1 : bits('datasize) = aget_Vpart(n, part);
   operand2 : bits('datasize) = aget_Vpart(m, part);
@@ -11836,7 +11836,7 @@ function aarch64_vector_arithmetic_binary_disparate_mul_poly ('d, 'datasize, 'el
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand1 : bits('datasize) = aget_Vpart(n, part);
   operand2 : bits('datasize) = aget_Vpart(m, part);
@@ -11858,7 +11858,7 @@ function aarch64_vector_arithmetic_binary_disparate_mul_double_sisd ('d, 'datasi
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand1 : bits('datasize) = aget_Vpart(n, part);
   operand2 : bits('datasize) = aget_Vpart(m, part);
@@ -11884,7 +11884,7 @@ function aarch64_vector_arithmetic_binary_disparate_mul_dmacc_sisd ('d, 'datasiz
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand1 : bits('datasize) = aget_Vpart(n, part);
   operand2 : bits('datasize) = aget_Vpart(m, part);
@@ -11916,7 +11916,7 @@ function aarch64_vector_arithmetic_binary_disparate_mul_accum ('d, 'datasize, 'e
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand1 : bits('datasize) = aget_Vpart(n, part);
   operand2 : bits('datasize) = aget_Vpart(m, part);
@@ -11943,7 +11943,7 @@ function aarch64_vector_arithmetic_binary_disparate_diff (accumulate, 'd, 'datas
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand1 : bits('datasize) = aget_Vpart(n, part);
   operand2 : bits('datasize) = aget_Vpart(m, part);
@@ -11968,7 +11968,7 @@ function aarch64_vector_arithmetic_binary_disparate_addsub_wide ('d, 'datasize,
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand1 : bits(2 * 'datasize) = aget_V(n);
   operand2 : bits('datasize) = aget_Vpart(m, part);
@@ -11992,7 +11992,7 @@ function aarch64_vector_arithmetic_binary_disparate_addsub_narrow ('d, 'datasize
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand1 : bits(2 * 'datasize) = aget_V(n);
   operand2 : bits(2 * 'datasize) = aget_V(m);
@@ -12018,7 +12018,7 @@ function aarch64_vector_arithmetic_binary_disparate_addsub_long ('d, 'datasize,
   assert(constraint('elements >= 1), "elements constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand1 : bits('datasize) = aget_Vpart(n, part);
   operand2 : bits('datasize) = aget_Vpart(m, part);
@@ -12039,7 +12039,7 @@ val aarch64_float_move_fp_select : (bits(4), int, int, int, int) -> unit effect
 
 function aarch64_float_move_fp_select (condition, 'd, 'datasize, 'm, 'n) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   result : bits('datasize) = if ConditionHolds(condition) then aget_V(n) else aget_V(m);
   aset_V(d, result)
@@ -12050,7 +12050,7 @@ val aarch64_float_move_fp_imm : forall ('datasize : Int).
 
 function aarch64_float_move_fp_imm ('d, datasize, imm) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   aset_V(d, imm)
 }
@@ -12127,7 +12127,7 @@ val aarch64_float_compare_uncond : (bool, int, int, int, bool) -> unit effect {e
 
 function aarch64_float_compare_uncond (cmp_with_zero, 'datasize, 'm, 'n, signal_all_nans) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand1 : bits('datasize) = aget_V(n);
   operand2 : bits('datasize) = if cmp_with_zero then FPZero(0b0) else aget_V(m);
@@ -12138,7 +12138,7 @@ val aarch64_float_compare_cond : (bits(4), int, bits(4), int, int, bool) -> unit
 
 function aarch64_float_compare_cond (condition, 'datasize, flags__arg, 'm, 'n, signal_all_nans) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   flags = flags__arg;
   CheckFPAdvSIMDEnabled64();
   operand1 : bits('datasize) = aget_V(n);
@@ -12151,7 +12151,7 @@ val aarch64_float_arithmetic_unary : (int, int, FPUnaryOp, int) -> unit effect {
 
 function aarch64_float_arithmetic_unary ('d, 'datasize, fpop, 'n) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   result : bits('datasize) = undefined;
   operand : bits('datasize) = aget_V(n);
@@ -12168,7 +12168,7 @@ val aarch64_float_arithmetic_round : (int, int, bool, int, FPRounding) -> unit e
 
 function aarch64_float_arithmetic_round ('d, 'datasize, exact, 'n, rounding) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   result : bits('datasize) = undefined;
   operand : bits('datasize) = aget_V(n);
@@ -12180,7 +12180,7 @@ val aarch64_float_arithmetic_mul_product : (int, int, int, int, bool) -> unit ef
 
 function aarch64_float_arithmetic_mul_product ('d, 'datasize, 'm, 'n, negated) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   result : bits('datasize) = undefined;
   operand1 : bits('datasize) = aget_V(n);
@@ -12194,7 +12194,7 @@ val aarch64_float_arithmetic_mul_addsub : (int, int, int, int, int, bool, bool)
 
 function aarch64_float_arithmetic_mul_addsub ('a, 'd, 'datasize, 'm, 'n, op1_neg, opa_neg) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   result : bits('datasize) = undefined;
   operanda : bits('datasize) = aget_V(a);
@@ -12210,7 +12210,7 @@ val aarch64_float_arithmetic_maxmin : (int, int, int, int, FPMaxMinOp) -> unit e
 
 function aarch64_float_arithmetic_maxmin ('d, 'datasize, 'm, 'n, operation) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   result : bits('datasize) = undefined;
   operand1 : bits('datasize) = aget_V(n);
@@ -12228,7 +12228,7 @@ val aarch64_float_arithmetic_div : (int, int, int, int) -> unit effect {escape,
 
 function aarch64_float_arithmetic_div ('d, 'datasize, 'm, 'n) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   result : bits('datasize) = undefined;
   operand1 : bits('datasize) = aget_V(n);
@@ -12241,7 +12241,7 @@ val aarch64_float_arithmetic_addsub : (int, int, int, int, bool) -> unit effect
 
 function aarch64_float_arithmetic_addsub ('d, 'datasize, 'm, 'n, sub_op) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   result : bits('datasize) = undefined;
   operand1 : bits('datasize) = aget_V(n);
@@ -12700,7 +12700,7 @@ function aarch64_memory_vector_single_nowb (datasize, esize, index, m, memop, n,
   element : bits('esize) = undefined;
   s : int = undefined;
   let 'ebytes : {'n, true. atom('n)} = ex_int(esize / 8);
-  assert(constraint(8 * 'ebytes = 'esize));
+  assert(constraint(8 * 'ebytes == 'esize));
   if n == 31 then {
     CheckSPAlignment();
     address = aget_SP()
@@ -12744,7 +12744,7 @@ function aarch64_memory_vector_multiple_nowb (datasize, elements, esize, m, memo
   s : int = undefined;
   tt : int = undefined;
   let 'ebytes = ex_int(esize / 8);
-  assert(constraint(8 * 'ebytes = 'esize));
+  assert(constraint(8 * 'ebytes == 'esize));
   if n == 31 then {
     CheckSPAlignment();
     address = aget_SP()
@@ -12774,7 +12774,7 @@ val aarch64_memory_single_simdfp_register : (AccType, int, ExtendType, int, MemO
 
 function aarch64_memory_single_simdfp_register (acctype, 'datasize, extend_type, 'm, memop, 'n, postindex, 'shift, 't, wback) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   offset : bits(64) = ExtendReg(m, extend_type, shift);
   CheckFPAdvSIMDEnabled64();
   address : bits(64) = undefined;
@@ -12804,7 +12804,7 @@ val aarch64_memory_single_simdfp_immediate_signed_postidx : (AccType, int, MemOp
 
 function aarch64_memory_single_simdfp_immediate_signed_postidx (acctype, 'datasize, memop, 'n, offset, postindex, 't, wback) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   address : bits(64) = undefined;
   data : bits('datasize) = undefined;
@@ -12833,7 +12833,7 @@ val aarch64_memory_single_simdfp_immediate_signed_offset_normal : (AccType, int,
 
 function aarch64_memory_single_simdfp_immediate_signed_offset_normal (acctype, 'datasize, memop, 'n, offset, postindex, 't, wback) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   address : bits(64) = undefined;
   data : bits('datasize) = undefined;
@@ -12866,7 +12866,7 @@ function aarch64_memory_ordered (acctype, datasize, memop, n, regsize, t) = {
   address : bits(64) = undefined;
   data : bits('datasize) = undefined;
   let 'dbytes = ex_int(datasize / 8);
-  assert(constraint(8 * 'dbytes = 'datasize));
+  assert(constraint(8 * 'dbytes == 'datasize));
   if n == 31 then {
     CheckSPAlignment();
     address = aget_SP()
@@ -12907,7 +12907,7 @@ function aarch64_memory_orderedrcpc (acctype, datasize, n, regsize, t) = {
   address : bits(64) = undefined;
   data : bits('datasize) = undefined;
   let 'dbytes = ex_int(datasize / 8);
-  assert(constraint(8 * 'dbytes = 'datasize));
+  assert(constraint(8 * 'dbytes == 'datasize));
   if n == 31 then {
     CheckSPAlignment();
     address = aget_SP()
@@ -12986,7 +12986,7 @@ function aarch64_memory_atomicops_swp ('datasize, ldacctype, 'n, 'regsize, 's, s
   assert(constraint('regsize >= 0), "regsize constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   address : bits(64) = undefined;
   data : bits('datasize) = undefined;
   if n == 31 then {
@@ -13002,7 +13002,7 @@ val aarch64_memory_atomicops_st : (int, AccType, int, MemAtomicOp, int, AccType)
 
 function aarch64_memory_atomicops_st ('datasize, ldacctype, 'n, op, 's, stacctype) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   address : bits(64) = undefined;
   value_name : bits('datasize) = undefined;
   data : bits('datasize) = undefined;
@@ -13032,7 +13032,7 @@ function aarch64_memory_atomicops_ld ('datasize, ldacctype, 'n, op, 'regsize, 's
   assert(constraint('regsize >= 0), "regsize constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   address : bits(64) = undefined;
   value_name : bits('datasize) = undefined;
   data : bits('datasize) = undefined;
@@ -13063,7 +13063,7 @@ function aarch64_memory_atomicops_cas_single ('datasize, ldacctype, 'n, 'regsize
   assert(constraint('regsize >= 0), "regsize constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   address : bits(64) = undefined;
   comparevalue : bits('datasize) = undefined;
   newvalue : bits('datasize) = undefined;
@@ -13085,7 +13085,7 @@ function aarch64_memory_atomicops_cas_pair ('datasize, ldacctype, 'n, 'regsize,
   assert(constraint('regsize >= 0), "regsize constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   address : bits(64) = undefined;
   comparevalue : bits(2 * 'datasize) = undefined;
   newvalue : bits(2 * 'datasize) = undefined;
@@ -13366,7 +13366,7 @@ function aarch64_memory_single_general_register (acctype, 'datasize, extend_type
   assert(constraint('regsize >= 0), "regsize constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   wback = wback__arg;
   offset : bits(64) = ExtendReg(m, extend_type, shift);
   address : bits(64) = undefined;
@@ -13422,7 +13422,7 @@ function aarch64_memory_single_general_immediate_unsigned (acctype, 'datasize, m
   assert(constraint('regsize >= 0), "regsize constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   wback = wback__arg;
   address : bits(64) = undefined;
   data : bits('datasize) = undefined;
@@ -13477,7 +13477,7 @@ function aarch64_memory_single_general_immediate_signed_postidx (acctype, 'datas
   assert(constraint('regsize >= 0), "regsize constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   wback = wback__arg;
   address : bits(64) = undefined;
   data : bits('datasize) = undefined;
@@ -13564,7 +13564,7 @@ function aarch64_memory_single_general_immediate_signed_offset_unpriv (acctype,
   assert(constraint('regsize >= 0), "regsize constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   wback = wback__arg;
   address : bits(64) = undefined;
   data : bits('datasize) = undefined;
@@ -13619,7 +13619,7 @@ function aarch64_memory_single_general_immediate_signed_offset_normal (acctype,
   assert(constraint('regsize >= 0), "regsize constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   wback = wback__arg;
   address : bits(64) = undefined;
   data : bits('datasize) = undefined;
@@ -13673,7 +13673,7 @@ val aarch64_memory_pair_simdfp_postidx : forall ('datasize : Int).
 
 function aarch64_memory_pair_simdfp_postidx (acctype, datasize, memop, n, offset, postindex, t, t2, wback) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   address : bits(64) = undefined;
   data1 : bits('datasize) = undefined;
@@ -13724,7 +13724,7 @@ val aarch64_memory_pair_simdfp_noalloc : forall ('datasize : Int).
 
 function aarch64_memory_pair_simdfp_noalloc (acctype, datasize, memop, n, offset, postindex, t, t2, wback) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   address : bits(64) = undefined;
   data1 : bits('datasize) = undefined;
@@ -13775,7 +13775,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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   wback = wback__arg;
   address : bits(64) = undefined;
   data1 : bits('datasize) = undefined;
@@ -13855,7 +13855,7 @@ val aarch64_memory_pair_general_noalloc : forall ('datasize : Int).
 
 function aarch64_memory_pair_general_noalloc (acctype, datasize, memop, n, offset, postindex, t, t2, wback) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   address : bits(64) = undefined;
   data1 : bits('datasize) = undefined;
   data2 : bits('datasize) = undefined;
@@ -13910,7 +13910,7 @@ function aarch64_memory_exclusive_single (acctype, datasize, elsize, memop, n, p
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
   assert(constraint(- 'elsize + 'datasize >= 0 & 'elsize >= 0));
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   address : bits(64) = undefined;
   data : bits('datasize) = undefined;
   rt_unknown : bool = false;
@@ -13957,7 +13957,7 @@ function aarch64_memory_exclusive_single (acctype, datasize, elsize, memop, n, p
     MemOp_STORE => {
       if rt_unknown then data = undefined
       else if pair then let 'v = ex_int(datasize / 2) in {
-        assert(constraint(2 * 'v = 'datasize));
+	assert(constraint(2 * 'v == 'datasize));
         el1 : bits('v) = aget_X(t);
         el2 : bits('v) = aget_X(t2);
         data = if BigEndian() then el1 @ el2 else el2 @ el1
@@ -14023,7 +14023,7 @@ function aarch64_memory_exclusive_pair (acctype, datasize, elsize, memop, n, pai
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
   assert(constraint(- 'elsize + 'datasize >= 0 & 'elsize >= 0), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   address : bits(64) = undefined;
   data : bits('datasize) = undefined;
   rt_unknown : bool = false;
@@ -14070,7 +14070,7 @@ function aarch64_memory_exclusive_pair (acctype, datasize, elsize, memop, n, pai
     MemOp_STORE => {
       if rt_unknown then data = undefined
       else if pair then let 'v = ex_int(datasize / 2) in {
-        assert(constraint(2 * 'v = 'datasize));
+	assert(constraint(2 * 'v == 'datasize));
         el1 : bits('v) = aget_X(t);
         el2 : bits('v) = aget_X(t2);
         data = if BigEndian() then el1 @ el2 else el2 @ el1
@@ -14305,7 +14305,7 @@ function vector_logical_decode (Q, op, a, b, c, cmode, o2, d, e, f, g, h, Rd) =
   };
   imm64 = AdvSIMDExpandImm(op, cmode, ((((((a @ b) @ c) @ d) @ e) @ f) @ g) @ h);
   let 'immsize = datasize / 64;
-  assert(constraint('immsize * 64 = 'datasize));
+  assert(constraint('immsize * 64 == 'datasize));
   imm = replicate_bits(imm64, 'immsize);
   aarch64_vector_logical(datasize, imm, operation, rd)
 }
@@ -14321,7 +14321,7 @@ function vector_fp16_movi_decode (Q, op, a, b, c, cmode, o2, d, e, f, g, h, Rd)
   imm8 : bits(8) = ((((((a @ b) @ c) @ d) @ e) @ f) @ g) @ h;
   imm16 : bits(16) = ((([imm8[7]] @ ~([imm8[6]])) @ replicate_bits([imm8[6]], 2)) @ slice(imm8, 0, 6)) @ Zeros(6);
   let 'immsize = datasize / 16;
-  assert(constraint('immsize * 16 = 'datasize));
+  assert(constraint('immsize * 16 == 'datasize));
   imm = replicate_bits(imm16, immsize);
   aarch64_vector_fp16_movi(datasize, imm, rd)
 }
diff --git a/aarch64/no_vector/spec.sail b/aarch64/no_vector/spec.sail
index 8710e66b..610884a4 100644
--- a/aarch64/no_vector/spec.sail
+++ b/aarch64/no_vector/spec.sail
@@ -1949,7 +1949,7 @@ val BigEndianReverse : forall ('width : Int), 'width >= 0 & 'width >= 0.
 function BigEndianReverse value_name = {
   assert('width == 8 | 'width == 16 | 'width == 32 | 'width == 64 | 'width == 128);
   let 'half = 'width / 2;
-  assert(constraint('half * 2 = 'width));
+  assert(constraint('half * 2 == 'width));
   if 'width == 8 then return(value_name) else ();
   return(BigEndianReverse(slice(value_name, 0, half)) @ BigEndianReverse(slice(value_name, half, 'width - half)))
 }
@@ -2065,7 +2065,7 @@ val Replicate : forall ('M : Int) ('N : Int), 'M >= 0 & 'N >= 0.
 function Replicate x = {
   assert('N % 'M == 0, "((N MOD M) == 0)");
   let 'O = 'N / 'M;
-  assert(constraint('O * 'M = 'N));
+  assert(constraint('O * 'M == 'N));
   return(replicate_bits(x, 'N / 'M))
 }
 
@@ -2721,7 +2721,7 @@ val aarch64_integer_insext_insert_movewide : (int, int, bits(16), MoveWideOp, in
 
 function aarch64_integer_insext_insert_movewide ('d, 'datasize, imm, opcode, 'pos) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   result : bits('datasize) = undefined;
   if opcode == MoveWideOp_K then result = aget_X(d) else result = Zeros();
   result = __SetSlice_bits(datasize, 16, result, pos, imm);
@@ -2733,7 +2733,7 @@ val aarch64_integer_insext_extract_immediate : (int, int, int, int, int) -> unit
 
 function aarch64_integer_insext_extract_immediate ('d, 'datasize, 'lsb, 'm, 'n) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   result : bits('datasize) = undefined;
   operand1 : bits('datasize) = aget_X(n);
   operand2 : bits('datasize) = aget_X(m);
@@ -2746,7 +2746,7 @@ val aarch64_integer_arithmetic_rev : (int, int, int, int) -> unit effect {escape
 
 function aarch64_integer_arithmetic_rev ('container_size, 'd, 'datasize, 'n) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   operand : bits('datasize) = aget_X(n);
   result : bits('datasize) = undefined;
   containers : int = datasize / container_size;
@@ -2768,7 +2768,7 @@ val aarch64_integer_arithmetic_rbit : (int, int, int) -> unit effect {escape, rr
 
 function aarch64_integer_arithmetic_rbit ('d, 'datasize, 'n) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   operand : bits('datasize) = aget_X(n);
   result : bits('datasize) = undefined;
   foreach (i from 0 to (datasize - 1) by 1 in inc)
@@ -2790,7 +2790,7 @@ val aarch64_integer_arithmetic_mul_widening_64128hi : (int, int, int, int, bool)
 
 function aarch64_integer_arithmetic_mul_widening_64128hi ('d, 'datasize, 'm, 'n, unsigned) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   operand1 : bits('datasize) = aget_X(n);
   operand2 : bits('datasize) = aget_X(m);
   result : int = asl_Int(operand1, unsigned) * asl_Int(operand2, unsigned);
@@ -2817,7 +2817,7 @@ function aarch64_integer_arithmetic_mul_widening_3264 ('a, 'd, 'datasize, 'dests
   assert(constraint('destsize in {32, 64}), "destsize constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   operand1 : bits('datasize) = aget_X(n);
   operand2 : bits('datasize) = aget_X(m);
   operand3 : bits('destsize) = aget_X(a);
@@ -2847,7 +2847,7 @@ function aarch64_integer_arithmetic_mul_uniform_addsub ('a, 'd, 'datasize, 'dest
   assert(constraint('destsize in {32, 64}), "destsize constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   operand1 : bits('datasize) = aget_X(n);
   operand2 : bits('datasize) = aget_X(m);
   operand3 : bits('destsize) = aget_X(a);
@@ -2874,7 +2874,7 @@ val aarch64_integer_arithmetic_div : (int, int, int, int, bool) -> unit effect {
 
 function aarch64_integer_arithmetic_div ('d, 'datasize, 'm, 'n, unsigned) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   operand1 : bits('datasize) = aget_X(n);
   operand2 : bits('datasize) = aget_X(m);
   result : int = undefined;
@@ -2898,7 +2898,7 @@ val aarch64_integer_arithmetic_cnt : (int, int, int, CountOp) -> unit effect {es
 
 function aarch64_integer_arithmetic_cnt ('d, 'datasize, 'n, opcode) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   result : int = undefined;
   operand1 : bits('datasize) = aget_X(n);
   if opcode == CountOp_CLZ then result = CountLeadingZeroBits(operand1) else result = CountLeadingSignBits(operand1);
@@ -2920,7 +2920,7 @@ val aarch64_integer_arithmetic_addsub_carry : (int, int, int, int, bool, bool) -
 
 function aarch64_integer_arithmetic_addsub_carry ('d, 'datasize, 'm, 'n, setflags, sub_op) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   result : bits('datasize) = undefined;
   operand1 : bits('datasize) = aget_X(n);
   operand2 : bits('datasize) = aget_X(m);
@@ -3042,7 +3042,7 @@ val aarch64_integer_bitfield : forall ('datasize : Int).
 
 function aarch64_integer_bitfield ('R, 'S, 'd, datasize, extend, inzero, 'n, tmask, wmask) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   dst : bits('datasize) = if inzero then Zeros() else aget_X(d);
   src : bits('datasize) = aget_X(n);
   bot : bits('datasize) = dst & ~(wmask) | ROR(src, R) & wmask;
@@ -3068,7 +3068,7 @@ val aarch64_integer_shift_variable : (int, int, int, int, ShiftType) -> unit eff
 
 function aarch64_integer_shift_variable ('d, 'datasize, 'm, 'n, shift_type) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   result : bits('datasize) = undefined;
   operand2 : bits('datasize) = aget_X(m);
   result = ShiftReg(n, shift_type, UInt(operand2) % datasize);
@@ -3091,7 +3091,7 @@ val aarch64_integer_logical_shiftedreg : (int, int, bool, int, int, LogicalOp, b
 
 function aarch64_integer_logical_shiftedreg ('d, 'datasize, invert, 'm, 'n, op, setflags, 'shift_amount, shift_type) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   operand1 : bits('datasize) = aget_X(n);
   operand2 : bits('datasize) = ShiftReg(m, shift_type, shift_amount);
   if invert then operand2 = ~(operand2) else ();
@@ -3109,7 +3109,7 @@ val aarch64_integer_arithmetic_addsub_shiftedreg : (int, int, int, int, bool, in
 
 function aarch64_integer_arithmetic_addsub_shiftedreg ('d, 'datasize, 'm, 'n, setflags, 'shift_amount, shift_type, sub_op) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   result : bits('datasize) = undefined;
   operand1 : bits('datasize) = aget_X(n);
   operand2 : bits('datasize) = ShiftReg(m, shift_type, shift_amount);
@@ -3244,7 +3244,7 @@ val aarch64_integer_logical_immediate : forall ('datasize : Int).
 
 function aarch64_integer_logical_immediate ('d, datasize, imm, 'n, op, setflags) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   result : bits('datasize) = undefined;
   operand1 : bits('datasize) = aget_X(n);
   operand2 : bits('datasize) = imm;
@@ -3262,7 +3262,7 @@ val aarch64_integer_arithmetic_addsub_immediate : forall ('datasize : Int).
 
 function aarch64_integer_arithmetic_addsub_immediate ('d, datasize, imm, 'n, setflags, sub_op) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   result : bits('datasize) = undefined;
   operand1 : bits('datasize) = if n == 31 then aget_SP() else aget_X(n);
   operand2 : bits('datasize) = imm;
@@ -3281,7 +3281,7 @@ val aarch64_integer_arithmetic_addsub_extendedreg : (int, int, ExtendType, int,
 
 function aarch64_integer_arithmetic_addsub_extendedreg ('d, 'datasize, extend_type, 'm, 'n, setflags, 'shift, sub_op) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   result : bits('datasize) = undefined;
   operand1 : bits('datasize) = if n == 31 then aget_SP() else aget_X(n);
   operand2 : bits('datasize) = ExtendReg(m, extend_type, shift);
@@ -4871,7 +4871,7 @@ val aarch64_integer_conditional_select : (bits(4), int, int, bool, bool, int, in
 
 function aarch64_integer_conditional_select (condition, 'd, 'datasize, else_inc, else_inv, 'm, 'n) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   result : bits('datasize) = undefined;
   operand1 : bits('datasize) = aget_X(n);
   operand2 : bits('datasize) = aget_X(m);
@@ -4901,7 +4901,7 @@ val aarch64_integer_conditional_compare_register : (bits(4), int, bits(4), int,
 
 function aarch64_integer_conditional_compare_register (condition, 'datasize, flags__arg, 'm, 'n, sub_op) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   flags = flags__arg;
   operand1 : bits('datasize) = aget_X(n);
   operand2 : bits('datasize) = aget_X(m);
@@ -4935,7 +4935,7 @@ val aarch64_integer_conditional_compare_immediate : forall ('datasize : Int).
 
 function aarch64_integer_conditional_compare_immediate (condition, datasize, flags__arg, imm, 'n, sub_op) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   flags = flags__arg;
   operand1 : bits('datasize) = aget_X(n);
   operand2 : bits('datasize) = imm;
@@ -6906,7 +6906,7 @@ val aarch64_branch_conditional_test : (int, bits(1), int, bits(64), int) -> unit
 
 function aarch64_branch_conditional_test ('bit_pos, bit_val, 'datasize, offset, 't) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   operand : bits('datasize) = aget_X(t);
   if [operand[bit_pos]] == bit_val then BranchTo(aget_PC() + offset, BranchType_JMP) else ()
 }
@@ -6940,7 +6940,7 @@ val aarch64_branch_conditional_compare : (int, bool, bits(64), int) -> unit effe
 
 function aarch64_branch_conditional_compare ('datasize, iszero, offset, 't) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   operand1 : bits('datasize) = aget_X(t);
   if IsZero(operand1) == iszero then BranchTo(aget_PC() + offset, BranchType_JMP) else ()
 }
@@ -8048,7 +8048,7 @@ val aarch64_float_move_fp_select : (bits(4), int, int, int, int) -> unit effect
 
 function aarch64_float_move_fp_select (condition, 'd, 'datasize, 'm, 'n) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   result : bits('datasize) = if ConditionHolds(condition) then aget_V(n) else aget_V(m);
   aset_V(d, result)
@@ -8059,7 +8059,7 @@ val aarch64_float_move_fp_imm : forall ('datasize : Int).
 
 function aarch64_float_move_fp_imm ('d, datasize, imm) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   aset_V(d, imm)
 }
@@ -8136,7 +8136,7 @@ val aarch64_float_compare_uncond : (bool, int, int, int, bool) -> unit effect {e
 
 function aarch64_float_compare_uncond (cmp_with_zero, 'datasize, 'm, 'n, signal_all_nans) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   operand1 : bits('datasize) = aget_V(n);
   operand2 : bits('datasize) = if cmp_with_zero then FPZero(0b0) else aget_V(m);
@@ -8147,7 +8147,7 @@ val aarch64_float_compare_cond : (bits(4), int, bits(4), int, int, bool) -> unit
 
 function aarch64_float_compare_cond (condition, 'datasize, flags__arg, 'm, 'n, signal_all_nans) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   flags = flags__arg;
   CheckFPAdvSIMDEnabled64();
   operand1 : bits('datasize) = aget_V(n);
@@ -8160,7 +8160,7 @@ val aarch64_float_arithmetic_unary : (int, int, FPUnaryOp, int) -> unit effect {
 
 function aarch64_float_arithmetic_unary ('d, 'datasize, fpop, 'n) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   result : bits('datasize) = undefined;
   operand : bits('datasize) = aget_V(n);
@@ -8177,7 +8177,7 @@ val aarch64_float_arithmetic_round : (int, int, bool, int, FPRounding) -> unit e
 
 function aarch64_float_arithmetic_round ('d, 'datasize, exact, 'n, rounding) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   result : bits('datasize) = undefined;
   operand : bits('datasize) = aget_V(n);
@@ -8189,7 +8189,7 @@ val aarch64_float_arithmetic_mul_product : (int, int, int, int, bool) -> unit ef
 
 function aarch64_float_arithmetic_mul_product ('d, 'datasize, 'm, 'n, negated) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   result : bits('datasize) = undefined;
   operand1 : bits('datasize) = aget_V(n);
@@ -8203,7 +8203,7 @@ val aarch64_float_arithmetic_mul_addsub : (int, int, int, int, int, bool, bool)
 
 function aarch64_float_arithmetic_mul_addsub ('a, 'd, 'datasize, 'm, 'n, op1_neg, opa_neg) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   result : bits('datasize) = undefined;
   operanda : bits('datasize) = aget_V(a);
@@ -8219,7 +8219,7 @@ val aarch64_float_arithmetic_maxmin : (int, int, int, int, FPMaxMinOp) -> unit e
 
 function aarch64_float_arithmetic_maxmin ('d, 'datasize, 'm, 'n, operation) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   result : bits('datasize) = undefined;
   operand1 : bits('datasize) = aget_V(n);
@@ -8237,7 +8237,7 @@ val aarch64_float_arithmetic_div : (int, int, int, int) -> unit effect {escape,
 
 function aarch64_float_arithmetic_div ('d, 'datasize, 'm, 'n) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   result : bits('datasize) = undefined;
   operand1 : bits('datasize) = aget_V(n);
@@ -8250,7 +8250,7 @@ val aarch64_float_arithmetic_addsub : (int, int, int, int, bool) -> unit effect
 
 function aarch64_float_arithmetic_addsub ('d, 'datasize, 'm, 'n, sub_op) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   result : bits('datasize) = undefined;
   operand1 : bits('datasize) = aget_V(n);
@@ -8535,7 +8535,7 @@ function aarch64_memory_vector_single_nowb (datasize, esize, index, m, memop, n,
   element : bits('esize) = undefined;
   s : int = undefined;
   let 'ebytes : {'n, true. atom('n)} = ex_int(esize / 8);
-  assert(constraint(8 * 'ebytes = 'esize));
+  assert(constraint(8 * 'ebytes == 'esize));
   if n == 31 then {
     CheckSPAlignment();
     address = aget_SP()
@@ -8579,7 +8579,7 @@ function aarch64_memory_vector_multiple_nowb (datasize, elements, esize, m, memo
   s : int = undefined;
   tt : int = undefined;
   let 'ebytes = ex_int(esize / 8);
-  assert(constraint(8 * 'ebytes = 'esize));
+  assert(constraint(8 * 'ebytes == 'esize));
   if n == 31 then {
     CheckSPAlignment();
     address = aget_SP()
@@ -8609,7 +8609,7 @@ val aarch64_memory_single_simdfp_register : (AccType, int, ExtendType, int, MemO
 
 function aarch64_memory_single_simdfp_register (acctype, 'datasize, extend_type, 'm, memop, 'n, postindex, 'shift, 't, wback) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   offset : bits(64) = ExtendReg(m, extend_type, shift);
   CheckFPAdvSIMDEnabled64();
   address : bits(64) = undefined;
@@ -8639,7 +8639,7 @@ val aarch64_memory_single_simdfp_immediate_signed_postidx : (AccType, int, MemOp
 
 function aarch64_memory_single_simdfp_immediate_signed_postidx (acctype, 'datasize, memop, 'n, offset, postindex, 't, wback) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   address : bits(64) = undefined;
   data : bits('datasize) = undefined;
@@ -8668,7 +8668,7 @@ val aarch64_memory_single_simdfp_immediate_signed_offset_normal : (AccType, int,
 
 function aarch64_memory_single_simdfp_immediate_signed_offset_normal (acctype, 'datasize, memop, 'n, offset, postindex, 't, wback) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   address : bits(64) = undefined;
   data : bits('datasize) = undefined;
@@ -8701,7 +8701,7 @@ function aarch64_memory_ordered (acctype, datasize, memop, n, regsize, t) = {
   address : bits(64) = undefined;
   data : bits('datasize) = undefined;
   let 'dbytes = ex_int(datasize / 8);
-  assert(constraint(8 * 'dbytes = 'datasize));
+  assert(constraint(8 * 'dbytes == 'datasize));
   if n == 31 then {
     CheckSPAlignment();
     address = aget_SP()
@@ -8742,7 +8742,7 @@ function aarch64_memory_orderedrcpc (acctype, datasize, n, regsize, t) = {
   address : bits(64) = undefined;
   data : bits('datasize) = undefined;
   let 'dbytes = ex_int(datasize / 8);
-  assert(constraint(8 * 'dbytes = 'datasize));
+  assert(constraint(8 * 'dbytes == 'datasize));
   if n == 31 then {
     CheckSPAlignment();
     address = aget_SP()
@@ -8821,7 +8821,7 @@ function aarch64_memory_atomicops_swp ('datasize, ldacctype, 'n, 'regsize, 's, s
   assert(constraint('regsize >= 0), "regsize constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   address : bits(64) = undefined;
   data : bits('datasize) = undefined;
   if n == 31 then {
@@ -8837,7 +8837,7 @@ val aarch64_memory_atomicops_st : (int, AccType, int, MemAtomicOp, int, AccType)
 
 function aarch64_memory_atomicops_st ('datasize, ldacctype, 'n, op, 's, stacctype) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   address : bits(64) = undefined;
   value_name : bits('datasize) = undefined;
   data : bits('datasize) = undefined;
@@ -8867,7 +8867,7 @@ function aarch64_memory_atomicops_ld ('datasize, ldacctype, 'n, op, 'regsize, 's
   assert(constraint('regsize >= 0), "regsize constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   address : bits(64) = undefined;
   value_name : bits('datasize) = undefined;
   data : bits('datasize) = undefined;
@@ -8898,7 +8898,7 @@ function aarch64_memory_atomicops_cas_single ('datasize, ldacctype, 'n, 'regsize
   assert(constraint('regsize >= 0), "regsize constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   address : bits(64) = undefined;
   comparevalue : bits('datasize) = undefined;
   newvalue : bits('datasize) = undefined;
@@ -8920,7 +8920,7 @@ function aarch64_memory_atomicops_cas_pair ('datasize, ldacctype, 'n, 'regsize,
   assert(constraint('regsize >= 0), "regsize constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   address : bits(64) = undefined;
   comparevalue : bits(2 * 'datasize) = undefined;
   newvalue : bits(2 * 'datasize) = undefined;
@@ -9201,7 +9201,7 @@ function aarch64_memory_single_general_register (acctype, 'datasize, extend_type
   assert(constraint('regsize >= 0), "regsize constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   wback = wback__arg;
   offset : bits(64) = ExtendReg(m, extend_type, shift);
   address : bits(64) = undefined;
@@ -9257,7 +9257,7 @@ function aarch64_memory_single_general_immediate_unsigned (acctype, 'datasize, m
   assert(constraint('regsize >= 0), "regsize constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   wback = wback__arg;
   address : bits(64) = undefined;
   data : bits('datasize) = undefined;
@@ -9312,7 +9312,7 @@ function aarch64_memory_single_general_immediate_signed_postidx (acctype, 'datas
   assert(constraint('regsize >= 0), "regsize constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   wback = wback__arg;
   address : bits(64) = undefined;
   data : bits('datasize) = undefined;
@@ -9399,7 +9399,7 @@ function aarch64_memory_single_general_immediate_signed_offset_unpriv (acctype,
   assert(constraint('regsize >= 0), "regsize constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   wback = wback__arg;
   address : bits(64) = undefined;
   data : bits('datasize) = undefined;
@@ -9454,7 +9454,7 @@ function aarch64_memory_single_general_immediate_signed_offset_normal (acctype,
   assert(constraint('regsize >= 0), "regsize constraint");
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   wback = wback__arg;
   address : bits(64) = undefined;
   data : bits('datasize) = undefined;
@@ -9508,7 +9508,7 @@ val aarch64_memory_pair_simdfp_postidx : forall ('datasize : Int).
 
 function aarch64_memory_pair_simdfp_postidx (acctype, datasize, memop, n, offset, postindex, t, t2, wback) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   address : bits(64) = undefined;
   data1 : bits('datasize) = undefined;
@@ -9559,7 +9559,7 @@ val aarch64_memory_pair_simdfp_noalloc : forall ('datasize : Int).
 
 function aarch64_memory_pair_simdfp_noalloc (acctype, datasize, memop, n, offset, postindex, t, t2, wback) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   CheckFPAdvSIMDEnabled64();
   address : bits(64) = undefined;
   data1 : bits('datasize) = undefined;
@@ -9610,7 +9610,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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   wback = wback__arg;
   address : bits(64) = undefined;
   data1 : bits('datasize) = undefined;
@@ -9690,7 +9690,7 @@ val aarch64_memory_pair_general_noalloc : forall ('datasize : Int).
 
 function aarch64_memory_pair_general_noalloc (acctype, datasize, memop, n, offset, postindex, t, t2, wback) = 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");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   address : bits(64) = undefined;
   data1 : bits('datasize) = undefined;
   data2 : bits('datasize) = undefined;
@@ -9745,7 +9745,7 @@ function aarch64_memory_exclusive_single (acctype, datasize, elsize, memop, n, p
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
   assert(constraint(- 'elsize + 'datasize >= 0 & 'elsize >= 0));
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   address : bits(64) = undefined;
   data : bits('datasize) = undefined;
   rt_unknown : bool = false;
@@ -9792,7 +9792,7 @@ function aarch64_memory_exclusive_single (acctype, datasize, elsize, memop, n, p
     MemOp_STORE => {
       if rt_unknown then data = undefined
       else if pair then let 'v = ex_int(datasize / 2) in {
-        assert(constraint(2 * 'v = 'datasize));
+	assert(constraint(2 * 'v == 'datasize));
         el1 : bits('v) = aget_X(t);
         el2 : bits('v) = aget_X(t2);
         data = if BigEndian() then el1 @ el2 else el2 @ el1
@@ -9858,7 +9858,7 @@ function aarch64_memory_exclusive_pair (acctype, datasize, elsize, memop, n, pai
   let 'dbytes = ex_int(datasize / 8);
   assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
   assert(constraint(- 'elsize + 'datasize >= 0 & 'elsize >= 0), "datasize constraint");
-  assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
+  assert(constraint(8 * 'dbytes == 'datasize), "dbytes constraint");
   address : bits(64) = undefined;
   data : bits('datasize) = undefined;
   rt_unknown : bool = false;
@@ -9905,7 +9905,7 @@ function aarch64_memory_exclusive_pair (acctype, datasize, elsize, memop, n, pai
     MemOp_STORE => {
       if rt_unknown then data = undefined
       else if pair then let 'v = ex_int(datasize / 2) in {
-        assert(constraint(2 * 'v = 'datasize));
+	assert(constraint(2 * 'v == 'datasize));
         el1 : bits('v) = aget_X(t);
         el2 : bits('v) = aget_X(t2);
         data = if BigEndian() then el1 @ el2 else el2 @ el1
diff --git a/editors/sail2-mode.el b/editors/sail2-mode.el
index eee0986f..e0081fb6 100644
--- a/editors/sail2-mode.el
+++ b/editors/sail2-mode.el
@@ -30,6 +30,7 @@
     (,(regexp-opt sail2-types 'symbols) . font-lock-type-face)
     (,(regexp-opt sail2-special 'symbols) . font-lock-preprocessor-face)
     ("~" . font-lock-negation-char-face)
+    ("\\(::\\)<" 1 font-lock-keyword-face)
     ("@" . font-lock-preprocessor-face)
     ("<->" . font-lock-negation-char-face)
     ("\'[a-zA-Z0-9_]+" . font-lock-variable-name-face)
diff --git a/lib/arith.sail b/lib/arith.sail
index db011f14..a3a80fc5 100644
--- a/lib/arith.sail
+++ b/lib/arith.sail
@@ -58,13 +58,13 @@ let elsize = shl_int(8, UInt(size))
 THIS ensures that in this case the typechecker knows that the end result will be a value in the set `{8, 16, 32, 64}`
 */
 val _shl8 = {c: "shl_mach_int", _: "shl_int"} :
-  forall 'n, 0 <= 'n <= 3. (int(8), int('n)) -> int('m) with 'm in {8, 16, 32, 64}
+  forall 'n, 0 <= 'n <= 3. (int(8), int('n)) -> {'m, 'm in {8, 16, 32, 64}. int('m)}
 
 /*!
 Similarly, we can shift 32 by either 0 or 1 to get a value in `{32, 64}`
 */
 val _shl32 = {c: "shl_mach_int", _: "shl_int"} :
-  forall 'n, 'n in {0, 1}. (int(32), int('n)) -> int('m) with 'm in {32, 64}
+  forall 'n, 'n in {0, 1}. (int(32), int('n)) -> {'m, 'm in {32, 64}. int('m)}
 
 val _shl_int = "shl_int" : (int, int) -> int
 
diff --git a/lib/option.sail b/lib/option.sail
index 3869167b..514cf7ba 100644
--- a/lib/option.sail
+++ b/lib/option.sail
@@ -6,7 +6,7 @@ $define _OPTION
 // this won't work - also no other type should be created with
 // constructors named Some or None.
 
-union option ('a : Type) = {
+union option('a: Type) = {
   Some : 'a,
   None : unit
 }
diff --git a/src/c_backend.ml b/src/c_backend.ml
index 326f742a..2f57a802 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -496,6 +496,9 @@ let analyze_primop' ctx id args typ =
 
   (* Optimized routines for all combinations of fixed and small bits
      appends, where the result is guaranteed to be smaller than 64. *)
+  | "append", [AV_C_fragment (vec1, _, CT_fbits (0, ord1)); AV_C_fragment (vec2, _, CT_fbits (n2, ord2)) as v2]
+       when ord1 = ord2 ->
+     AE_val v2
   | "append", [AV_C_fragment (vec1, _, CT_fbits (n1, ord1)); AV_C_fragment (vec2, _, CT_fbits (n2, ord2))]
        when ord1 = ord2 && n1 + n2 <= 64 ->
      AE_val (AV_C_fragment (F_op (F_op (vec1, "<<", v_int n2), "|", vec2), typ, CT_fbits (n1 + n2, ord1)))
diff --git a/src/lexer.mll b/src/lexer.mll
index f5a982eb..a1f3ace2 100644
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -217,6 +217,7 @@ rule token = parse
   | "@"                                 { (At "@") }
   | "2" ws "^"                          { TwoCaret }
   | "^"					{ (Caret(r"^")) }
+  | "::<"                               { ColonColonLt }
   | "::"                                { ColonColon(r "::") }
   (* | "^^"                                { CaretCaret(r "^^") } *)
   | "~~"                                { TildeTilde(r "~~") }
diff --git a/src/parser.mly b/src/parser.mly
index fec38669..8287060c 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -133,6 +133,8 @@ let mk_tannot typq typ n m = Typ_annot_opt_aux(Typ_annot_opt_some (typq, typ), l
 let mk_eannotn = Effect_opt_aux(Effect_opt_pure,Unknown)
 let mk_namesectn = Name_sect_aux(Name_sect_none,Unknown)
 
+let mk_typq kopts nc n m = TypQ_aux (TypQ_tq (List.map qi_id_of_kopt kopts @ nc), loc n m)
+
 type lchain =
   LC_lt
 | LC_lteq
@@ -171,6 +173,8 @@ let rec desugar_rchain chain s e =
     mk_nc (NC_and (nc1, desugar_rchain (RC_nexp n2 :: chain) s e)) s e
   | _ -> assert false
 
+let future_syntax l = Util.warn (Reporting.loc_to_string l ^ "\n\nThis syntax is currently experimental")
+
 %}
 
 /*Terminals with no content*/
@@ -185,7 +189,7 @@ let rec desugar_rchain chain s e =
 %nonassoc Then
 %nonassoc Else
 
-%token Bar Comma Dot Eof Minus Semi Under DotDot
+%token Bar Comma Dot Eof Minus Semi Under DotDot ColonColonLt
 %token Lcurly Rcurly Lparen Rparen Lsquare Rsquare LcurlyBar RcurlyBar LsquareBar RsquareBar
 %token MinusGt Bidir LtMinus
 
@@ -196,7 +200,7 @@ let rec desugar_rchain chain s e =
 %token <string> String Bin Hex Real
 
 %token <string> Amp At Caret Eq Gt Lt Plus Star EqGt Unit
-%token <string> Colon ColonColon (* CaretCaret *) TildeTilde ExclEq
+%token <string> Colon ColonColon TildeTilde ExclEq
 %token <string> EqEq
 %token <string> GtEq
 %token <string> LtEq
@@ -339,9 +343,6 @@ atomic_nc:
     { mk_nc NC_true $startpos $endpos }
   | False
     { mk_nc NC_false $startpos $endpos }
-  | typ0 Eq typ0
-    { Util.warn ("Deprecated syntax, use == instead at " ^ Reporting.loc_to_string (loc $startpos($2) $endpos($2)) ^ "\n");
-      mk_nc (NC_equal ($1, $3)) $startpos $endpos }
   | typ0 EqEq typ0
     { mk_nc (NC_equal ($1, $3)) $startpos $endpos }
   | typ0 ExclEq typ0
@@ -355,38 +356,6 @@ atomic_nc:
   | kid In Lcurly num_list Rcurly
     { mk_nc (NC_set ($1, $4)) $startpos $endpos }
 
-new_nc:
-  | new_nc Bar new_nc_and
-    { mk_nc (NC_or ($1, $3)) $startpos $endpos }
-  | nc_and
-    { $1 }
-
-new_nc_and:
-  | new_nc_and Amp new_atomic_nc
-    { mk_nc (NC_and ($1, $3)) $startpos $endpos }
-  | new_atomic_nc
-    { $1 }
-
-new_atomic_nc:
-  | Where id Lparen typ_list Rparen
-    { mk_nc (NC_app ($2, $4)) $startpos $endpos }
-  | True
-    { mk_nc NC_true $startpos $endpos }
-  | False
-    { mk_nc NC_false $startpos $endpos }
-  | typ0 EqEq typ0
-    { mk_nc (NC_equal ($1, $3)) $startpos $endpos }
-  | typ0 ExclEq typ0
-    { mk_nc (NC_not_equal ($1, $3)) $startpos $endpos }
-  | nc_lchain
-    { desugar_lchain $1 $startpos $endpos }
-  | nc_rchain
-    { desugar_rchain $1 $startpos $endpos }
-  | Lparen new_nc Rparen
-    { $2 }
-  | kid In Lcurly num_list Rcurly
-    { mk_nc (NC_set ($1, $4)) $startpos $endpos }
-
 num_list:
   | Num
     { [$1] }
@@ -413,11 +382,17 @@ nc_rchain:
   | typ0 Gt nc_rchain
     { RC_nexp $1 :: RC_gt :: $3 }
 
+tyarg:
+  | ColonColonLt typ_list Gt
+    { future_syntax (loc $startpos($1) $endpos($3)); $2, [] }
+  | Lparen typ_list Rparen
+    { [], $2 }
+  | ColonColonLt typ_list Gt Lparen typ_list Rparen
+    { future_syntax (loc $startpos($1) $endpos($3)); $2, $5 }
+
 typ:
   | typ0
     { $1 }
-  | typ0 With new_nc
-    { mk_typ (ATyp_with ($1, $3)) $startpos $endpos }
 
 /* The following implements all nine levels of user-defined precedence for
 operators in types, with both left, right and non-associative operators */
@@ -587,8 +562,8 @@ atomic_typ:
     { mk_typ ATyp_dec $startpos $endpos }
   | Inc
     { mk_typ ATyp_inc $startpos $endpos }
-  | id Lparen typ_list Rparen
-    { mk_typ (ATyp_app ($1, $3)) $startpos $endpos }
+  | id tyarg
+    { mk_typ (ATyp_app ($1, snd $2 @ fst $2)) $startpos $endpos }
   | Register Lparen typ Rparen
     { let register_id = mk_id (Id "register") $startpos($1) $endpos($1) in
       mk_typ (ATyp_app (register_id, [$3])) $startpos $endpos }
@@ -1193,14 +1168,43 @@ r_def_body:
   | r_id_def Comma r_def_body
     { $1 :: $3 }
 
+param_kopt:
+  | kid Colon kind
+    { KOpt_aux (KOpt_kind ($3, $1), loc $startpos $endpos) }
+  | kid
+    { KOpt_aux (KOpt_none $1, loc $startpos $endpos) }
+
+param_kopt_list:
+  | param_kopt
+    { [$1] }
+  | param_kopt Comma param_kopt_list
+    { $1 :: $3 }
+
+typaram:
+  | ColonColonLt param_kopt_list Gt Lparen param_kopt_list Rparen Comma nc
+    { future_syntax (loc $startpos($1) $endpos($3));
+      let qi_nc = QI_aux (QI_const $8, loc $startpos($8) $endpos($8)) in
+      mk_typq ($5 @ $2) [qi_nc] $startpos $endpos }
+  | ColonColonLt param_kopt_list Gt Lparen param_kopt_list Rparen
+    { future_syntax (loc $startpos($1) $endpos($3));
+      mk_typq ($5 @ $2) [] $startpos $endpos }
+  | ColonColonLt param_kopt_list Gt
+    { future_syntax (loc $startpos($1) $endpos($3));
+      mk_typq $2 [] $startpos $endpos }
+  | Lparen param_kopt_list Rparen Comma nc
+    { let qi_nc = QI_aux (QI_const $5, loc $startpos($5) $endpos($5)) in
+      mk_typq $2 [qi_nc] $startpos $endpos }
+  | Lparen param_kopt_list Rparen
+    { mk_typq $2 [] $startpos $endpos }
+
 type_def:
-  | Typedef id typquant Eq typ
+  | Typedef id typaram Eq typ
     { mk_td (TD_abbrev ($2, mk_namesectn, mk_typschm $3 $5 $startpos($3) $endpos)) $startpos $endpos }
   | Typedef id Eq typ
     { mk_td (TD_abbrev ($2, mk_namesectn, mk_typschm mk_typqn $4 $startpos($4) $endpos)) $startpos $endpos }
   | Struct id Eq Lcurly struct_fields Rcurly
     { mk_td (TD_record ($2, mk_namesectn, TypQ_aux (TypQ_tq [], loc $endpos($2) $startpos($3)), $5, false)) $startpos $endpos }
-  | Struct id typquant Eq Lcurly struct_fields Rcurly
+  | Struct id typaram Eq Lcurly struct_fields Rcurly
     { mk_td (TD_record ($2, mk_namesectn, $3, $6, false)) $startpos $endpos }
   | Enum id Eq enum_bar
     { mk_td (TD_enum ($2, mk_namesectn, $4, false)) $startpos $endpos }
@@ -1208,11 +1212,11 @@ type_def:
     { mk_td (TD_enum ($2, mk_namesectn, $5, false)) $startpos $endpos }
   | Newtype id Eq type_union
     { mk_td (TD_variant ($2, mk_namesectn, TypQ_aux (TypQ_tq [], loc $endpos($2) $startpos($3)), [$4], false)) $startpos $endpos }
-  | Newtype id typquant Eq type_union
+  | Newtype id typaram Eq type_union
     { mk_td (TD_variant ($2, mk_namesectn, $3, [$5], false)) $startpos $endpos }
   | Union id Eq Lcurly type_unions Rcurly
     { mk_td (TD_variant ($2, mk_namesectn, TypQ_aux (TypQ_tq [], loc $endpos($2) $startpos($3)), $5, false)) $startpos $endpos }
-  | Union id typquant Eq Lcurly type_unions Rcurly
+  | Union id typaram Eq Lcurly type_unions Rcurly
     { mk_td (TD_variant ($2, mk_namesectn, $3, $6, false)) $startpos $endpos }
   | Bitfield id Colon typ Eq Lcurly r_def_body Rcurly
     { mk_td (TD_bitfield ($2, $4, $7)) $startpos $endpos }
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index a2771ae1..53e77df2 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -151,7 +151,7 @@ let doc_nc nc =
     | NC_and (c1, c2) -> separate space [nc1 c1; string "&"; atomic_nc c2]
     | _ -> atomic_nc nc
   in
-  nc0 ~parenthesize:true (constraint_simp nc)
+  atomic_nc (constraint_simp nc)
 
 let rec doc_typ ?(simple=false) (Typ_aux (typ_aux, l)) =
   match typ_aux with
@@ -219,6 +219,27 @@ let doc_quants quants =
   | [nc] -> kdoc ^^ comma ^^ space ^^ doc_nc nc
   | nc :: ncs -> kdoc ^^ comma ^^ space ^^ doc_nc (List.fold_left nc_and nc ncs)
 
+let doc_param_quants quants =
+  let doc_qi_kopt (QI_aux (qi_aux, _)) =
+    match qi_aux with
+    | QI_id (KOpt_aux (KOpt_none kid, _)) -> [doc_kid kid]
+    | QI_id kopt when is_nat_kopt kopt -> [doc_kid (kopt_kid kopt) ^^ colon ^^ space ^^ string "Int"]
+    | QI_id kopt when is_typ_kopt kopt -> [doc_kid (kopt_kid kopt) ^^ colon ^^ space ^^ string "Type"]
+    | QI_id kopt -> [doc_kid (kopt_kid kopt) ^^ colon ^^ space ^^ string "Order"]
+    | QI_const nc -> []
+  in
+  let qi_nc (QI_aux (qi_aux, _)) =
+    match qi_aux with
+    | QI_const nc -> [nc]
+    | _ -> []
+  in
+  let kdoc = separate (comma ^^ space) (List.concat (List.map doc_qi_kopt quants)) in
+  let ncs = List.concat (List.map qi_nc quants) in
+  match ncs with
+  | [] -> parens kdoc
+  | [nc] -> parens kdoc ^^ comma ^^ space ^^ doc_nc nc
+  | nc :: ncs -> parens kdoc ^^ comma ^^ space ^^ doc_nc (List.fold_left nc_and nc ncs)
+
 let doc_binding ?(simple=false) ((TypQ_aux (tq_aux, _) as typq), typ) =
   match tq_aux with
   | TypQ_no_forall -> doc_typ ~simple:simple typ
@@ -244,7 +265,7 @@ let doc_typschm_quants (TypSchm_aux (TypSchm_ts (TypQ_aux (tq_aux, _), typ), _))
   match tq_aux with
   | TypQ_no_forall -> None
   | TypQ_tq [] -> None
-  | TypQ_tq qs -> Some (doc_quants qs)
+  | TypQ_tq qs -> Some (doc_param_quants qs)
 
 let doc_lit (L_aux(l,_)) =
   utf8string (match l with
@@ -547,7 +568,7 @@ let doc_typdef (TD_aux(td,_)) = match td with
      begin
        match doc_typschm_quants typschm with
        | Some qdoc ->
-          doc_op equals (concat [string "type"; space; doc_id id; space; qdoc]) (doc_typschm_typ typschm)
+          doc_op equals (concat [string "type"; space; doc_id id; qdoc]) (doc_typschm_typ typschm)
        | None ->
           doc_op equals (concat [string "type"; space; doc_id id]) (doc_typschm_typ typschm)
      end
@@ -556,12 +577,12 @@ let doc_typdef (TD_aux(td,_)) = match td with
   | TD_record (id, _, TypQ_aux (TypQ_no_forall, _), fields, _) | TD_record (id, _, TypQ_aux (TypQ_tq [], _), fields, _) ->
      separate space [string "struct"; doc_id id; equals; surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_field fields) rbrace]
   | TD_record (id, _, TypQ_aux (TypQ_tq qs, _), fields, _) ->
-     separate space [string "struct"; doc_id id; doc_quants qs; equals;
+     separate space [string "struct"; doc_id id; doc_param_quants qs; equals;
                      surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_field fields) rbrace]
   | TD_variant (id, _, TypQ_aux (TypQ_no_forall, _), unions, _) | TD_variant (id, _, TypQ_aux (TypQ_tq [], _), unions, _) ->
      separate space [string "union"; doc_id id; equals; surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_union unions) rbrace]
   | TD_variant (id, _, TypQ_aux (TypQ_tq qs, _), unions, _) ->
-     separate space [string "union"; doc_id id; doc_quants qs; equals;
+     separate space [string "union"; doc_id id; doc_param_quants qs; equals;
                      surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_union unions) rbrace]
   | _ -> string "TYPEDEF"
 
diff --git a/test/c/cheri128_hsb.sail b/test/c/cheri128_hsb.sail
index a06a2ad2..d8501d88 100644
--- a/test/c/cheri128_hsb.sail
+++ b/test/c/cheri128_hsb.sail
@@ -14,7 +14,7 @@ val add_range = {ocaml: "add_int", lem: "integerAdd", coq: "add_range", c: "add_
 val sub_range = {ocaml: "sub_int", lem: "integerMinus", coq: "sub_range"} : forall 'n 'm 'o 'p.
   (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o)
 
-val min = {ocaml: "min_int", lem: "min", coq: "min_atom", c:"min_int"} : forall 'a 'b . (atom('a), atom('b)) -> {'c, ('c = 'a | 'c = 'b) & 'c <= 'a & 'c <= 'b . atom('c)}
+val min = {ocaml: "min_int", lem: "min", coq: "min_atom", c:"min_int"} : forall 'a 'b . (atom('a), atom('b)) -> {'c, ('c == 'a | 'c == 'b) & 'c <= 'a & 'c <= 'b . atom('c)}
 
 overload operator + = {add_range}
 overload operator - = {sub_range}
diff --git a/test/c/poly_pair.sail b/test/c/poly_pair.sail
index 6d0bdaad..c4989829 100644
--- a/test/c/poly_pair.sail
+++ b/test/c/poly_pair.sail
@@ -4,7 +4,7 @@ val print = "print_endline" : string -> unit
 
 val "eq_int" : (int, int) -> bool
 
-union test ('a : Type) ('b : Type) = {
+union test('a : Type, 'b : Type) = {
   Ctor1 : ('a, 'b),
   Ctor2 : int
 }
diff --git a/test/ocaml/reg_ref/rr.sail b/test/ocaml/reg_ref/rr.sail
index d0a14586..f162d3a2 100644
--- a/test/ocaml/reg_ref/rr.sail
+++ b/test/ocaml/reg_ref/rr.sail
@@ -33,7 +33,7 @@ overload _mod_GPR = { rGPR, wGPR }
 /* Create a new type which is a pair of a bitvector and a start index
 
    slice('n, 'm) is equivalent to old-sail vector('n, 'm, dec, bit) */
-newtype slice ('n : Int) ('m : Int) = MkSlice : (atom('n), bits('m))
+newtype slice ('n : Int, 'm : Int) = MkSlice : (atom('n), bits('m))
 
 /* Extract the bitvector from a slice */
 val slice_bits : forall 'n 'm. slice('n, 'm) -> bits('m)
@@ -76,7 +76,7 @@ overload _mod_slice = {_set_slice, _set_slice2, vector_slice, slice_slice}
 /* Set up a struct with an aliased LT bit in CR0, mimicing old-style syntax */
 infix 1 ...
 
-type operator ... ('n : Int) ('m : Int) = slice('m, 'n - ('m - 1))
+type operator ...('n : Int, 'm : Int) = slice('m, 'n - ('m - 1))
 
 struct cr = {
   CR0 : 7 ... 4,
diff --git a/test/ocaml/void/void.sail b/test/ocaml/void/void.sail
index 485ac019..4e8815f5 100644
--- a/test/ocaml/void/void.sail
+++ b/test/ocaml/void/void.sail
@@ -1,5 +1,5 @@
 
-val void : forall 'n, 'n = 'n + 1. atom('n) -> unit
+val void : forall 'n, 'n == 'n + 1. atom('n) -> unit
 
 function void _ = ()
 
diff --git a/test/typecheck/pass/bind_typ_var.sail b/test/typecheck/pass/bind_typ_var.sail
index c442d6a8..ae340941 100644
--- a/test/typecheck/pass/bind_typ_var.sail
+++ b/test/typecheck/pass/bind_typ_var.sail
@@ -1,7 +1,7 @@
 
 val mk_vector : unit -> {'n, 'n in {32, 64}. vector('n, dec, bit)}
 
-val mk_square : unit -> {'n 'm, 'n = 'm. vector('n, dec, vector('m, dec, bit))}
+val mk_square : unit -> {'n 'm, 'n == 'm. vector('n, dec, vector('m, dec, bit))}
 
 val test : unit -> unit
 
@@ -10,8 +10,8 @@ function test () = {
   // could still be
   let v2 as 'len2 = mk_vector ();
   let matrix as vector('width, _, 'height) = mk_square ();
-  _prove(constraint('width = 'height));
-  _prove(constraint('len = 32 | 'len = 64));
-  _prove(constraint('len2 = 32 | 'len2 = 64));
+  _prove(constraint('width == 'height));
+  _prove(constraint('len == 32 | 'len == 64));
+  _prove(constraint('len2 == 32 | 'len2 == 64));
   ()
 }
 \ No newline at end of file
diff --git a/test/typecheck/pass/constrained_struct.sail b/test/typecheck/pass/constrained_struct.sail
index 64b2287f..87d55b65 100644
--- a/test/typecheck/pass/constrained_struct.sail
+++ b/test/typecheck/pass/constrained_struct.sail
@@ -2,7 +2,7 @@ default Order dec
 
 $include <prelude.sail>
 
-struct MyStruct 'n, 'n in {32, 64} = {
+struct MyStruct('n), 'n in {32, 64} = {
   field: bits('n)
 }
 
diff --git a/test/typecheck/pass/constrained_struct/v1.sail b/test/typecheck/pass/constrained_struct/v1.sail
index 62fc1c01..98daf59e 100644
--- a/test/typecheck/pass/constrained_struct/v1.sail
+++ b/test/typecheck/pass/constrained_struct/v1.sail
@@ -2,7 +2,7 @@ default Order dec
 
 $include <prelude.sail>
 
-struct MyStruct 'n, 'n in {32, 64} = {
+struct MyStruct('n), 'n in {32, 64} = {
   field: bits('n)
 }
 
diff --git a/test/typecheck/pass/exint.sail b/test/typecheck/pass/exint.sail
index ffa6d033..3e2acf28 100644
--- a/test/typecheck/pass/exint.sail
+++ b/test/typecheck/pass/exint.sail
@@ -1,8 +1,8 @@
 type MyInt = {'n, true. atom('n)}
 
-val add : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o = 'n + 'm. atom('o)}
+val add : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o == 'n + 'm. atom('o)}
 
-val mult : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o = 'n * 'm. atom('o)}
+val mult : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o == 'n * 'm. atom('o)}
 
 overload operator + = {add}
 
@@ -14,7 +14,7 @@ let y = x + x * x
 
 let z : atom(7 * 8) = y
 
-type Range ('n : Int) ('m : Int), 'n <= 'm = {'o, 'n <= 'o & 'o <= 'm. atom('o)}
+type Range('n: Int, 'm: Int), 'n <= 'm = {'o, 'n <= 'o & 'o <= 'm. atom('o)}
 
 let a : Range(3, 4) = 3
 
diff --git a/test/typecheck/pass/exist1.sail b/test/typecheck/pass/exist1.sail
index f6c0c073..6db518e8 100644
--- a/test/typecheck/pass/exist1.sail
+++ b/test/typecheck/pass/exist1.sail
@@ -22,6 +22,6 @@ function unit_fn x : atom(4) = ()
 
 val s_add : forall 'a. (atom('a), atom('a)) -> atom('a + 'a)
 
-let v7 : {'k, 'k = 4. atom('k)} = 4
+let v7 : {'k, 'k == 4. atom('k)} = 4
 
 let v8 = s_add(v7, 4)
diff --git a/test/typecheck/pass/exist2.sail b/test/typecheck/pass/exist2.sail
index 42ec8cb1..102a1084 100644
--- a/test/typecheck/pass/exist2.sail
+++ b/test/typecheck/pass/exist2.sail
@@ -22,13 +22,13 @@ function unit_fn x : atom(4) = ()
 
 val s_add : forall 'a. (atom('a), atom('a)) -> atom('a + 'a)
 
-let v7 : {'k, 'k = 4. atom('k)} = 4
+let v7 : {'k, 'k == 4. atom('k)} = 4
 
-let v9 : {'n, 0 = 0. atom('n)} = 100
+let v9 : {'n, 0 == 0. atom('n)} = 100
 
 let v10 : int = v9
 
-type MyInt = {'n, 0 = 0. atom('n)}
+type MyInt = {'n, 0 == 0. atom('n)}
 
 val existential_int : int -> MyInt
 
@@ -37,7 +37,7 @@ val existential_range : forall 'n 'm.
 
 overload existential = {existential_int, existential_range}
 
-let v11 : {'n, 0 = 0. atom('n)} = existential(v10)
+let v11 : {'n, 0 == 0. atom('n)} = existential(v10)
 
 let v12 : {'e, 0 <= 'e & 'e <= 3. atom('e)} = existential(2 : range(0, 3))
 
diff --git a/test/typecheck/pass/exist_synonym.sail b/test/typecheck/pass/exist_synonym.sail
index 44382213..b251cbf8 100644
--- a/test/typecheck/pass/exist_synonym.sail
+++ b/test/typecheck/pass/exist_synonym.sail
@@ -1,6 +1,6 @@
 
 // Type synonym with a constraint.
-type regno ('n : Int), 0 <= 'n < 32 = atom('n)
+type regno('n: Int), 0 <= 'n < 32 = atom('n)
 
 // Existential with constrained type synonym.
 let x : {'n, 0 <= 'n <= 8. regno('n)} = 4
diff --git a/test/typecheck/pass/exist_synonym/v1.expect b/test/typecheck/pass/exist_synonym/v1.expect
index 3169f619..583c4485 100644
--- a/test/typecheck/pass/exist_synonym/v1.expect
+++ b/test/typecheck/pass/exist_synonym/v1.expect
@@ -2,6 +2,6 @@ Type error at file "exist_synonym/v1.sail", line 6, character 42 to line 6, char
 
 let x : {'n, 0 <= 'n <= 33. regno('n)} = [41m4[0m
 
-Tried performing type coercion from int(4) to {'n, 0 <= 'n & 'n <= 33. regno('n)} on 4
+Tried performing type coercion from int(4) to {'n, (0 <= 'n & 'n <= 33). regno('n)} on 4
 Failed because
 Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym int('n) with (0 <= 'n & 'n <= 33)
diff --git a/test/typecheck/pass/exist_synonym/v2.expect b/test/typecheck/pass/exist_synonym/v2.expect
index 02b1c17a..baddbcb0 100644
--- a/test/typecheck/pass/exist_synonym/v2.expect
+++ b/test/typecheck/pass/exist_synonym/v2.expect
@@ -2,6 +2,6 @@ Type error at file "exist_synonym/v2.sail", line 6, character 41 to line 6, char
 
 let x : {'n, 0 <= 'n <= 8. regno('n)} = [41m4[0m
 
-Tried performing type coercion from int(4) to {'n, 0 <= 'n & 'n <= 8. regno('n)} on 4
+Tried performing type coercion from int(4) to {'n, (0 <= 'n & 'n <= 8). regno('n)} on 4
 Failed because
 Could not prove constraints (0 <= 'n & ('n + 1) <= 2) in type synonym int('n) with (0 <= 'n & 'n <= 8)
diff --git a/test/typecheck/pass/option_either.sail b/test/typecheck/pass/option_either.sail
index 24e50259..ec4e72db 100644
--- a/test/typecheck/pass/option_either.sail
+++ b/test/typecheck/pass/option_either.sail
@@ -1,6 +1,6 @@
 default Order inc
 
-union option ('a : Type) = {None : unit, Some : 'a}
+union option('a: Type) = {None : unit, Some : 'a}
 
 function none forall ('a : Type). () -> option('a) = None()
 
@@ -11,7 +11,7 @@ function test forall ('a : Type). x : option('a) -> range(0, 1) = match x {
   Some(y) => 1
 }
 
-union either ('a : Type) ('b : Type) = {Left : 'a, Right : 'b}
+union either('a: Type, 'b: Type) = {Left : 'a, Right : 'b}
 
 val signed : forall ('n : Int), 'n >= 0. vector('n, inc, bit) -> int
 
diff --git a/test/typecheck/pass/pure_record2.sail b/test/typecheck/pass/pure_record2.sail
index cbdb2c9d..588fd324 100644
--- a/test/typecheck/pass/pure_record2.sail
+++ b/test/typecheck/pass/pure_record2.sail
@@ -1,6 +1,6 @@
 default Order dec
 
-struct State ('a : Type) ('n : Int) = {
+struct State('a: Type, 'n: Int) = {
   N : vector('n, dec, 'a),
   Z : vector(1, dec, bit)
 }
diff --git a/test/typecheck/pass/pure_record3.sail b/test/typecheck/pass/pure_record3.sail
index cd3e849a..de388c3e 100644
--- a/test/typecheck/pass/pure_record3.sail
+++ b/test/typecheck/pass/pure_record3.sail
@@ -1,6 +1,6 @@
 default Order dec
 
-struct State ('a : Type) ('n : Int) = {
+struct State('a: Type, 'n: Int) = {
   N : vector('n, dec, 'a),
   Z : vector(1, dec, bit)
 }
author	Alasdair Armstrong	2018-11-30 18:54:42 +0000
committer	Alasdair Armstrong	2018-11-30 19:13:39 +0000
commit	0363a325ca6c498e086519c4ecaf1f51dbff7f64 (patch)
tree	bb40aa476726b365bed73c02f1184147eda394cf
parent	e25d469d7dfccc46db663ebcd4e00a5bfcac499a (diff)