///|
pub(all) enum IntUnaryOp {
  Not
  CountLeadingZeros
  CountTrailingZeros
  PopulationCount
} derive(Debug, Eq, Hash)

///|
pub(all) enum IntBinaryOp {
  Add
  Sub
  Mul
  SignedDiv
  UnsignedDiv
  SignedRem
  UnsignedRem
  And
  Or
  Xor
  ShiftLeft
  SignedShiftRight
  UnsignedShiftRight
  RotateLeft
  RotateRight
} derive(Debug, Eq, Hash)

///|
pub(all) enum IntComparison {
  Equal
  NotEqual
  SignedLessThan
  SignedLessOrEqual
  SignedGreaterThan
  SignedGreaterOrEqual
  UnsignedLessThan
  UnsignedLessOrEqual
  UnsignedGreaterThan
  UnsignedGreaterOrEqual
} derive(Debug, Eq, Hash)

///|
pub(all) enum IntOverflowOp {
  Add(@native.Signedness)
  Sub(@native.Signedness)
  Mul(@native.Signedness)
} derive(Debug, Eq, Hash)

///|
pub(all) enum FloatUnaryOp {
  Negate
  Absolute
  SquareRoot
  Ceil
  Floor
  Truncate
  Nearest
} derive(Debug, Eq, Hash)

///|
pub(all) enum FloatBinaryOp {
  Add
  Sub
  Mul
  Div
  Min
  Max
  CopySign
} derive(Debug, Eq, Hash)

///|
pub(all) enum FloatTernaryOp {
  FusedMultiplyAdd
  FusedNegatedMultiplyAdd
  FusedMultiplySubtract
  FusedNegatedMultiplySubtract
} derive(Debug, Eq, Hash)

///|
pub(all) enum FloatComparison {
  Equal
  NotEqual
  LessThan
  LessOrEqual
  GreaterThan
  GreaterOrEqual
  Ordered
  Unordered
} derive(Debug, Eq, Hash)

///|
pub(all) enum ReferenceComparison {
  Equal
  NotEqual
} derive(Debug, Eq, Hash)

///|
pub(all) enum ConversionOp {
  I32WrapI64
  I64ExtendI32(@native.Signedness)
  F32DemoteF64
  F64PromoteF32
  FloatToInt(
    @native.FloatType,
    @native.IntegerType,
    @native.Signedness,
    @native.ConversionMode
  )
  IntToFloat(@native.IntegerType, @native.FloatType, @native.Signedness)
  SignExtend(@native.IntegerType, @native.AccessWidth)
  Bitcast(@native.ValueType, @native.ValueType)
} derive(Debug, Eq, Hash)

///|
pub struct LoadSpec {
  width : @native.AccessWidth
  extension : @native.LoadExtension
  result_type : @native.ValueType
  offset : UInt64
  endianness : @native.Endianness
  trap : @native.TrapReason?
} derive(Debug, Eq, Hash)

///|
pub fn LoadSpec::new(
  width : @native.AccessWidth,
  extension : @native.LoadExtension,
  result_type : @native.ValueType,
  offset : UInt64,
  endianness : @native.Endianness,
  trap : @native.TrapReason?,
) -> LoadSpec {
  { width, extension, result_type, offset, endianness, trap, }
}

///|
pub struct StoreSpec {
  width : @native.AccessWidth
  value_type : @native.ValueType
  offset : UInt64
  endianness : @native.Endianness
  trap : @native.TrapReason?
} derive(Debug, Eq, Hash)

///|
pub fn StoreSpec::new(
  width : @native.AccessWidth,
  value_type : @native.ValueType,
  offset : UInt64,
  endianness : @native.Endianness,
  trap : @native.TrapReason?,
) -> StoreSpec {
  { width, value_type, offset, endianness, trap, }
}

///|
pub(all) enum AtomicRmwOp {
  Add
  Sub
  And
  Or
  Xor
  Exchange
} derive(Debug, Eq, Hash)

///|
/// A sequentially consistent atomic memory access. Weaker memory orders are
/// not part of the current native-lowering contract.
pub struct AtomicSpec {
  width : @native.AccessWidth
  value_type : @native.ValueType
  offset : UInt64
  endianness : @native.Endianness
  trap : @native.TrapReason?
} derive(Debug, Eq, Hash)

///|
pub fn AtomicSpec::new(
  width : @native.AccessWidth,
  value_type : @native.ValueType,
  offset : UInt64,
  endianness : @native.Endianness,
  trap : @native.TrapReason?,
) -> AtomicSpec {
  { width, value_type, offset, endianness, trap, }
}

///|
pub(all) enum VectorLane {
  I8x16
  I16x8
  I32x4
  I64x2
  F32x4
  F64x2
} derive(Debug, Eq, Hash)

///|
pub(all) enum VectorBitwiseOp {
  Not
  And
  Or
  Xor
  AndNot
  BitSelect
} derive(Debug, Eq, Hash)

///|
pub(all) enum VectorIntUnaryOp {
  Absolute
  Negate
  PopulationCount
  ExtendAddPairwise(@native.Signedness)
} derive(Debug, Eq, Hash)

///|
pub(all) enum VectorHalf {
  Low
  High
} derive(Debug, Eq, Hash)

///|
pub(all) enum VectorIntBinaryOp {
  Add
  Sub
  Mul
  Min(@native.Signedness)
  Max(@native.Signedness)
  AverageUnsigned
  SaturatingAdd(@native.Signedness)
  SaturatingSub(@native.Signedness)
  ExtendMultiply(VectorHalf, @native.Signedness)
  Dot16To32Signed
  Q15MultiplyRoundedSaturating
} derive(Debug, Eq, Hash)

///|
pub(all) enum VectorIntShiftOp {
  Left
  Right(@native.Signedness)
} derive(Debug, Eq, Hash)

///|
pub(all) enum VectorIntComparison {
  Equal
  NotEqual
  LessThan(@native.Signedness)
  LessOrEqual(@native.Signedness)
  GreaterThan(@native.Signedness)
  GreaterOrEqual(@native.Signedness)
} derive(Debug, Eq, Hash)

///|
pub(all) enum VectorFloatUnaryOp {
  Absolute
  Negate
  SquareRoot
  Ceil
  Floor
  Truncate
  Nearest
} derive(Debug, Eq, Hash)

///|
pub(all) enum VectorFloatBinaryOp {
  Add
  Sub
  Mul
  Div
  Min
  Max
  PseudoMin
  PseudoMax
} derive(Debug, Eq, Hash)

///|
pub(all) enum VectorFloatComparison {
  Equal
  NotEqual
  LessThan
  LessOrEqual
  GreaterThan
  GreaterOrEqual
} derive(Debug, Eq, Hash)

///|
pub(all) enum VectorPredicateOp {
  AnyTrue
  AllTrue(VectorLane)
  BitMask(VectorLane)
} derive(Debug, Eq, Hash)

///|
pub(all) enum VectorConversionOp {
  ExtendLow(VectorLane, @native.Signedness)
  ExtendHigh(VectorLane, @native.Signedness)
  Narrow(VectorLane, @native.Signedness)
  FloatToInt(VectorLane, VectorLane, @native.Signedness, @native.ConversionMode)
  IntToFloat(VectorLane, VectorLane, @native.Signedness)
  PromoteLowF32x4
  DemoteZeroF64x2
} derive(Debug, Eq, Hash)

///|
pub(all) enum VectorRelaxedOp {
  Swizzle
  FloatToInt(VectorLane, VectorLane, @native.Signedness)
  FusedMultiplyAdd(VectorLane, FloatTernaryOp)
  LaneSelect(VectorLane)
  Min(VectorLane)
  Max(VectorLane)
  Q15MultiplyRoundedSigned
  Dot8To16Signed
  Dot8To32AddSigned
} derive(Debug, Eq, Hash)

///|
pub(all) enum VectorLoadKind {
  Splat(VectorLane)
  Extend(VectorLane, @native.Signedness)
  Zero(@native.AccessWidth)
  Lane(VectorLane, Int)
} derive(Debug, Eq, Hash)

///|
pub struct VectorLoadSpec {
  kind : VectorLoadKind
  offset : UInt64
  endianness : @native.Endianness
  trap : @native.TrapReason?
} derive(Debug, Eq, Hash)

///|
pub fn VectorLoadSpec::new(
  kind : VectorLoadKind,
  offset : UInt64,
  endianness : @native.Endianness,
  trap : @native.TrapReason?,
) -> VectorLoadSpec {
  { kind, offset, endianness, trap, }
}

///|
pub struct VectorStoreLaneSpec {
  lane : VectorLane
  lane_index : Int
  offset : UInt64
  endianness : @native.Endianness
  trap : @native.TrapReason?
} derive(Debug, Eq, Hash)

///|
pub fn VectorStoreLaneSpec::new(
  lane : VectorLane,
  lane_index : Int,
  offset : UInt64,
  endianness : @native.Endianness,
  trap : @native.TrapReason?,
) -> VectorStoreLaneSpec {
  { lane, lane_index, offset, endianness, trap, }
}

///|
pub(all) enum VectorOp {
  Splat(VectorLane)
  ExtractLane(VectorLane, Int, @native.Signedness?)
  ReplaceLane(VectorLane, Int)
  Shuffle(FixedArray[Int])
  Swizzle
  Bitwise(VectorBitwiseOp)
  IntUnary(VectorLane, VectorIntUnaryOp)
  IntBinary(VectorLane, VectorIntBinaryOp)
  IntShift(VectorLane, VectorIntShiftOp)
  IntCompare(VectorLane, VectorIntComparison)
  FloatUnary(VectorLane, VectorFloatUnaryOp)
  FloatBinary(VectorLane, VectorFloatBinaryOp)
  FloatTernary(VectorLane, FloatTernaryOp)
  FloatCompare(VectorLane, VectorFloatComparison)
  Predicate(VectorPredicateOp)
  Convert(VectorConversionOp)
  Relaxed(VectorRelaxedOp)
} derive(Debug, Eq)

///|
pub(all) enum Operation {
  I32Const(UInt)
  I64Const(UInt64)
  F32Const(UInt)
  F64Const(UInt64)
  V128Const(UInt64, UInt64)
  NullPtr
  NullGcRef
  CodeAddress(@native.CodeSymbol)
  ExternalAddress(@native.ExternalSymbol)
  DataAddress(@native.DataSymbol)
  EnvironmentField(@native.EnvironmentField, @native.EnvironmentFieldStability)
  StackAddress(@native.StackObject)
  Copy
  Select
  GcRefAddress
  GcRefFromBits
  PointerOffset
  ReferenceCompare(ReferenceComparison)
  IntUnary(IntUnaryOp)
  IntBinary(IntBinaryOp)
  IntBinaryImmediate(IntBinaryOp, UInt64)
  IntShiftImmediate(IntBinaryOp, Int)
  IntMultiplyAdd
  IntAddShiftedLeft(Int)
  IntHighMultiply(@native.Signedness)
  IntWithOverflow(IntOverflowOp)
  IntCompare(IntComparison)
  FloatUnary(FloatUnaryOp)
  FloatBinary(FloatBinaryOp)
  FloatTernary(FloatTernaryOp)
  FloatCompare(FloatComparison)
  Convert(ConversionOp)
  Load(LoadSpec)
  LoadIndexed(LoadSpec, Int)
  Store(StoreSpec)
  StoreIndexed(StoreSpec, Int)
  AtomicLoad(AtomicSpec)
  AtomicStore(AtomicSpec)
  AtomicRmw(AtomicSpec, AtomicRmwOp)
  AtomicCompareExchange(AtomicSpec)
  AtomicFence
  Vector(VectorOp)
  VectorLoad(VectorLoadSpec)
  VectorStoreLane(VectorStoreLaneSpec)
  Call(@native.NativeCall)
  Safepoint(@native.SafepointKind)
} derive(Debug, Eq)

///|
fn VectorOp::copy(self : VectorOp) -> VectorOp {
  match self {
    Shuffle(mask) =>
      Shuffle(FixedArray::makei(mask.length(), index => mask[index]))
    Splat(_)
    | ExtractLane(_, _, _)
    | ReplaceLane(_, _)
    | Swizzle
    | Bitwise(_)
    | IntUnary(_, _)
    | IntBinary(_, _)
    | IntShift(_, _)
    | IntCompare(_, _)
    | FloatUnary(_, _)
    | FloatBinary(_, _)
    | FloatTernary(_, _)
    | FloatCompare(_, _)
    | Predicate(_)
    | Convert(_)
    | Relaxed(_) => self
  }
}

///|
pub fn Operation::copy(self : Operation) -> Operation {
  match self {
    Vector(operation) => Vector(operation.copy())
    Call(call) => Call(call)
    I32Const(_)
    | I64Const(_)
    | F32Const(_)
    | F64Const(_)
    | V128Const(_, _)
    | NullPtr
    | NullGcRef
    | CodeAddress(_)
    | ExternalAddress(_)
    | DataAddress(_)
    | EnvironmentField(_, _)
    | StackAddress(_)
    | Copy
    | Select
    | GcRefAddress
    | GcRefFromBits
    | PointerOffset
    | ReferenceCompare(_)
    | IntUnary(_)
    | IntBinary(_)
    | IntBinaryImmediate(_, _)
    | IntShiftImmediate(_, _)
    | IntMultiplyAdd
    | IntAddShiftedLeft(_)
    | IntHighMultiply(_)
    | IntWithOverflow(_)
    | IntCompare(_)
    | FloatUnary(_)
    | FloatBinary(_)
    | FloatTernary(_)
    | FloatCompare(_)
    | Convert(_)
    | Load(_)
    | LoadIndexed(_, _)
    | Store(_)
    | StoreIndexed(_, _)
    | AtomicLoad(_)
    | AtomicStore(_)
    | AtomicRmw(_, _)
    | AtomicCompareExchange(_)
    | AtomicFence
    | VectorLoad(_)
    | VectorStoreLane(_)
    | Safepoint(_) => self
  }
}

///|
fn integer_value_type(ty : @native.IntegerType) -> @native.ValueType {
  match ty {
    I32 => I32
    I64 => I64
  }
}

///|
fn float_value_type(ty : @native.FloatType) -> @native.ValueType {
  match ty {
    F32 => F32
    F64 => F64
  }
}

///|
fn is_integer_type(ty : @native.ValueType) -> Bool {
  ty == I32 || ty == I64
}

///|
fn is_float_type(ty : @native.ValueType) -> Bool {
  ty == F32 || ty == F64
}

///|
fn scalar_type_for_lane(lane : VectorLane) -> @native.ValueType {
  match lane {
    I8x16 | I16x8 | I32x4 => I32
    I64x2 => I64
    F32x4 => F32
    F64x2 => F64
  }
}

///|
fn is_integer_lane(lane : VectorLane) -> Bool {
  match lane {
    I8x16 | I16x8 | I32x4 | I64x2 => true
    F32x4 | F64x2 => false
  }
}

///|
fn is_float_lane(lane : VectorLane) -> Bool {
  !is_integer_lane(lane)
}

///|
fn lane_count(lane : VectorLane) -> Int {
  match lane {
    I8x16 => 16
    I16x8 => 8
    I32x4 | F32x4 => 4
    I64x2 | F64x2 => 2
  }
}

///|
fn is_widened_integer_lane(lane : VectorLane) -> Bool {
  lane == I16x8 || lane == I32x4 || lane == I64x2
}

///|
fn verify_vector_conversion(op : VectorConversionOp) -> String? {
  match op {
    ExtendLow(lane, _) | ExtendHigh(lane, _) =>
      if is_widened_integer_lane(lane) {
        None
      } else {
        operation_error(
          "vector extension destination must be i16x8, i32x4, or i64x2",
        )
      }
    Narrow(lane, _) =>
      if lane == I8x16 || lane == I16x8 {
        None
      } else {
        operation_error("vector narrowing destination must be i8x16 or i16x8")
      }
    FloatToInt(source, result, _, _) =>
      if (source == F32x4 && result == I32x4) ||
        (source == F64x2 && result == I32x4) {
        None
      } else {
        operation_error(
          "vector float-to-int conversion requires f32x4 or f64x2 source and i32x4 result",
        )
      }
    IntToFloat(source, result, _) =>
      if source == I32x4 && (result == F32x4 || result == F64x2) {
        None
      } else {
        operation_error(
          "vector int-to-float conversion requires i32x4 source and f32x4 or f64x2 result",
        )
      }
    PromoteLowF32x4 | DemoteZeroF64x2 => None
  }
}

///|
fn verify_relaxed_vector_operation(
  op : VectorRelaxedOp,
  operands : Array[@native.ValueType],
  results : Array[@native.ValueType],
) -> String? {
  match op {
    Swizzle =>
      require_shape(
        operands,
        results,
        [V128, V128],
        [V128],
        "vector.relaxed_swizzle",
      )
    FloatToInt(source, result, _) =>
      match
        verify_vector_conversion(FloatToInt(source, result, Signed, Saturating)) {
        Some(error) => Some(error)
        None =>
          require_shape(
            operands,
            results,
            [V128],
            [V128],
            "vector.relaxed_float_to_int",
          )
      }
    FusedMultiplyAdd(lane, _) => {
      if !is_float_lane(lane) {
        return operation_error(
          "relaxed fused multiply-add requires floating lanes",
        )
      }
      require_shape(
        operands,
        results,
        [V128, V128, V128],
        [V128],
        "vector.relaxed_fma",
      )
    }
    LaneSelect(lane) => {
      if !is_integer_lane(lane) {
        return operation_error("relaxed lane select requires integer lanes")
      }
      require_shape(
        operands,
        results,
        [V128, V128, V128],
        [V128],
        "vector.relaxed_lane_select",
      )
    }
    Min(lane) | Max(lane) => {
      if !is_float_lane(lane) {
        return operation_error("relaxed min/max requires floating lanes")
      }
      require_shape(
        operands,
        results,
        [V128, V128],
        [V128],
        "vector.relaxed_minmax",
      )
    }
    Q15MultiplyRoundedSigned =>
      require_shape(
        operands,
        results,
        [V128, V128],
        [V128],
        "vector.relaxed_q15mulr",
      )
    Dot8To16Signed =>
      require_shape(
        operands,
        results,
        [V128, V128],
        [V128],
        "vector.relaxed_dot8_to16",
      )
    Dot8To32AddSigned =>
      require_shape(
        operands,
        results,
        [V128, V128, V128],
        [V128],
        "vector.relaxed_dot8_to32_add",
      )
  }
}

///|
fn width_bits(width : @native.AccessWidth) -> Int {
  match width {
    W8 => 8
    W16 => 16
    W32 => 32
    W64 => 64
    W128 => 128
  }
}

///|
fn value_type_bits(ty : @native.ValueType) -> Int {
  match ty {
    I32 | F32 => 32
    I64 | F64 | Ptr64 | GcRef64 => 64
    V128 => 128
  }
}

///|
fn operation_error(message : String) -> String? {
  Some(message)
}

///|
fn require_shape(
  operands : Array[@native.ValueType],
  results : Array[@native.ValueType],
  expected_operands : Array[@native.ValueType],
  expected_results : Array[@native.ValueType],
  name : String,
) -> String? {
  if operands != expected_operands {
    return operation_error(
      "\{name} expects operands \{Repr(expected_operands)}, got \{Repr(operands)}",
    )
  }
  if results != expected_results {
    return operation_error(
      "\{name} expects results \{Repr(expected_results)}, got \{Repr(results)}",
    )
  }
  None
}

///|
fn verify_load_spec(spec : LoadSpec) -> String? {
  let result_bits = value_type_bits(spec.result_type)
  let access_bits = width_bits(spec.width)
  if spec.result_type == V128 {
    if spec.width != W128 || spec.extension != None {
      return operation_error("v128 load requires width 128 without extension")
    }
  } else if spec.result_type == Ptr64 || spec.result_type == GcRef64 {
    if spec.width != W64 || spec.extension != None {
      return operation_error(
        "pointer and GC-reference loads require width 64 without extension",
      )
    }
  } else if is_float_type(spec.result_type) {
    if result_bits != access_bits || spec.extension != None {
      return operation_error(
        "floating loads require an equal-width access without extension",
      )
    }
  } else if access_bits > result_bits {
    return operation_error("load width exceeds its result width")
  } else if access_bits == result_bits && spec.extension != None {
    return operation_error("equal-width integer load cannot extend")
  } else if access_bits < result_bits && spec.extension == None {
    return operation_error("narrow integer load requires signedness")
  }
  None
}

///|
fn verify_store_spec(spec : StoreSpec) -> String? {
  let access_bits = width_bits(spec.width)
  let value_bits = value_type_bits(spec.value_type)
  if spec.value_type == V128 {
    if spec.width != W128 {
      return operation_error("v128 store requires width 128")
    }
  } else if spec.value_type == Ptr64 || spec.value_type == GcRef64 {
    if spec.width != W64 {
      return operation_error("pointer and GC-reference stores require width 64")
    }
  } else if is_float_type(spec.value_type) && access_bits != value_bits {
    return operation_error("floating stores require an equal-width access")
  } else if access_bits > value_bits {
    return operation_error("store width exceeds its value width")
  }
  None
}

///|
fn verify_atomic_spec(spec : AtomicSpec) -> String? {
  if !is_integer_type(spec.value_type) {
    return operation_error("atomic values must be i32 or i64")
  }
  let bits = width_bits(spec.width)
  if bits > value_type_bits(spec.value_type) || bits == 128 {
    return operation_error("atomic width exceeds its integer value type")
  }
  None
}

///|
fn verify_vector_operation(
  op : VectorOp,
  operands : Array[@native.ValueType],
  results : Array[@native.ValueType],
) -> String? {
  match op {
    Splat(lane) =>
      require_shape(
        operands,
        results,
        [scalar_type_for_lane(lane)],
        [V128],
        "vector.splat",
      )
    ExtractLane(lane, index, extension) => {
      if index < 0 || index >= lane_count(lane) {
        return operation_error("vector.extract_lane index is out of range")
      }
      if is_float_lane(lane) || lane == I32x4 || lane == I64x2 {
        if extension is Some(_) {
          return operation_error(
            "full-width and floating lane extraction cannot extend",
          )
        }
      } else if extension is None {
        return operation_error(
          "narrow integer lane extraction requires signedness",
        )
      }
      require_shape(
        operands,
        results,
        [V128],
        [scalar_type_for_lane(lane)],
        "vector.extract_lane",
      )
    }
    ReplaceLane(lane, index) => {
      if index < 0 || index >= lane_count(lane) {
        return operation_error("vector.replace_lane index is out of range")
      }
      require_shape(
        operands,
        results,
        [V128, scalar_type_for_lane(lane)],
        [V128],
        "vector.replace_lane",
      )
    }
    Shuffle(mask) => {
      if mask.length() != 16 {
        return operation_error(
          "vector.shuffle requires exactly 16 lane indices",
        )
      }
      for lane in mask {
        if lane < 0 || lane >= 32 {
          return operation_error("vector.shuffle lane index is out of range")
        }
      }
      require_shape(operands, results, [V128, V128], [V128], "vector.shuffle")
    }
    Swizzle =>
      require_shape(operands, results, [V128, V128], [V128], "vector.swizzle")
    Bitwise(kind) => {
      let arity = match kind {
        Not => 1
        And | Or | Xor | AndNot => 2
        BitSelect => 3
      }
      require_shape(
        operands,
        results,
        Array::make(arity, V128),
        [V128],
        "vector.bitwise",
      )
    }
    IntUnary(lane, operation) => {
      if !is_integer_lane(lane) {
        return operation_error(
          "vector integer unary operation requires integer lanes",
        )
      }
      if operation is ExtendAddPairwise(_) && !is_widened_integer_lane(lane) {
        return operation_error(
          "pairwise extending add destination must be i16x8, i32x4, or i64x2",
        )
      }
      if operation == PopulationCount && lane != I8x16 {
        return operation_error("vector population count requires i8x16 lanes")
      }
      require_shape(operands, results, [V128], [V128], "vector.int_unary")
    }
    IntBinary(lane, operation) => {
      if !is_integer_lane(lane) {
        return operation_error(
          "vector integer operation requires integer lanes",
        )
      }
      match operation {
        ExtendMultiply(_, _) =>
          if !is_widened_integer_lane(lane) {
            return operation_error(
              "extending multiply destination must be i16x8, i32x4, or i64x2",
            )
          }
        Dot16To32Signed =>
          if lane != I32x4 {
            return operation_error(
              "dot16-to32 requires i32x4 destination lanes",
            )
          }
        Q15MultiplyRoundedSaturating =>
          if lane != I16x8 {
            return operation_error(
              "q15 rounded saturating multiply requires i16x8 lanes",
            )
          }
        AverageUnsigned =>
          if lane != I8x16 && lane != I16x8 {
            return operation_error(
              "vector unsigned average requires i8x16 or i16x8 lanes",
            )
          }
        Add
        | Sub
        | Mul
        | Min(_)
        | Max(_)
        | SaturatingAdd(_)
        | SaturatingSub(_) => ()
      }
      require_shape(
        operands,
        results,
        [V128, V128],
        [V128],
        "vector.int_binary",
      )
    }
    IntCompare(lane, _) => {
      if !is_integer_lane(lane) {
        return operation_error(
          "vector integer comparison requires integer lanes",
        )
      }
      require_shape(
        operands,
        results,
        [V128, V128],
        [V128],
        "vector.int_compare",
      )
    }
    IntShift(lane, _) => {
      if !is_integer_lane(lane) {
        return operation_error("vector integer shift requires integer lanes")
      }
      require_shape(operands, results, [V128, I32], [V128], "vector.int_shift")
    }
    FloatUnary(lane, _) => {
      if !is_float_lane(lane) {
        return operation_error(
          "vector float unary operation requires float lanes",
        )
      }
      require_shape(operands, results, [V128], [V128], "vector.float_unary")
    }
    FloatBinary(lane, _) | FloatCompare(lane, _) => {
      if !is_float_lane(lane) {
        return operation_error("vector float operation requires float lanes")
      }
      require_shape(
        operands,
        results,
        [V128, V128],
        [V128],
        "vector.float_binary",
      )
    }
    FloatTernary(lane, _) => {
      if !is_float_lane(lane) {
        return operation_error("vector float operation requires float lanes")
      }
      require_shape(
        operands,
        results,
        [V128, V128, V128],
        [V128],
        "vector.float_ternary",
      )
    }
    Predicate(_) =>
      require_shape(operands, results, [V128], [I32], "vector.predicate")
    Convert(conversion) =>
      match verify_vector_conversion(conversion) {
        Some(error) => Some(error)
        None => {
          let operand_types = match conversion {
            Narrow(_, _) => [@native.V128, V128]
            _ => [V128]
          }
          require_shape(
            operands,
            results,
            operand_types,
            [V128],
            "vector.convert",
          )
        }
      }
    Relaxed(operation) =>
      verify_relaxed_vector_operation(operation, operands, results)
  }
}

///|
fn verify_vector_load_spec(spec : VectorLoadSpec) -> String? {
  match spec.kind {
    Splat(_) => None
    Extend(lane, _) =>
      match lane {
        I16x8 | I32x4 | I64x2 => None
        I8x16 | F32x4 | F64x2 =>
          operation_error(
            "vector load-extend requires i16x8, i32x4, or i64x2 destination lanes",
          )
      }
    Zero(width) =>
      if width == W32 || width == W64 {
        None
      } else {
        operation_error("vector load-zero requires width 32 or 64")
      }
    Lane(lane, lane_index) =>
      if lane_index < 0 || lane_index >= lane_count(lane) {
        operation_error("vector load-lane index is out of range")
      } else {
        None
      }
  }
}

///|
fn verify_vector_store_lane_spec(spec : VectorStoreLaneSpec) -> String? {
  if spec.lane_index < 0 || spec.lane_index >= lane_count(spec.lane) {
    operation_error("vector store-lane index is out of range")
  } else {
    None
  }
}

///|
fn call_operand_types(call : @native.NativeCall) -> Array[@native.ValueType] {
  let types = call.signature.params.copy()
  if call.callee is Indirect {
    types.insert(0, Ptr64)
  }
  types
}

///|
pub fn verify_call_operands(
  call : @native.NativeCall,
  operands : Array[@native.ValueType],
  context : String,
) -> String? {
  match call.callee {
    Internal(symbol) =>
      if symbol.name.is_empty() {
        return operation_error("\{context} internal symbol must not be empty")
      }
    External(symbol) =>
      if symbol.name.is_empty() {
        return operation_error("\{context} external symbol must not be empty")
      }
    Indirect => ()
  }
  let expected = call_operand_types(call)
  if operands != expected {
    return operation_error(
      "\{context} expects operands \{Repr(expected)}, got \{Repr(operands)}",
    )
  }
  None
}

///|
pub fn verify_operation_contract(
  op : Operation,
  operands : Array[@native.ValueType],
  results : Array[@native.ValueType],
) -> String? {
  match op {
    I32Const(_) => require_shape(operands, results, [], [I32], "i32.const")
    I64Const(_) => require_shape(operands, results, [], [I64], "i64.const")
    F32Const(_) => require_shape(operands, results, [], [F32], "f32.const")
    F64Const(_) => require_shape(operands, results, [], [F64], "f64.const")
    V128Const(_, _) =>
      require_shape(operands, results, [], [V128], "v128.const")
    NullPtr => require_shape(operands, results, [], [Ptr64], "ptr.null")
    NullGcRef => require_shape(operands, results, [], [GcRef64], "gcref.null")
    CodeAddress(symbol) =>
      if symbol.name.is_empty() {
        operation_error("code symbol must not be empty")
      } else {
        require_shape(operands, results, [], [Ptr64], "code.address")
      }
    ExternalAddress(symbol) =>
      if symbol.name.is_empty() {
        operation_error("external symbol must not be empty")
      } else {
        require_shape(operands, results, [], [Ptr64], "external.address")
      }
    DataAddress(symbol) =>
      if symbol.name.is_empty() {
        operation_error("data symbol must not be empty")
      } else {
        require_shape(operands, results, [], [Ptr64], "data.address")
      }
    EnvironmentField(field, _) =>
      if field.name.is_empty() {
        operation_error("environment field identity must not be empty")
      } else {
        require_shape(
          operands,
          results,
          [Ptr64],
          [field.value_type],
          "environment.field",
        )
      }
    StackAddress(_) =>
      require_shape(operands, results, [], [Ptr64], "stack.address")
    Copy => {
      if operands.length() != 1 || results.length() != 1 {
        return operation_error("copy expects one operand and one result")
      }
      if operands[0] != results[0] {
        return operation_error("copy operand and result types must match")
      }
      None
    }
    Select => {
      if operands.length() != 3 || results.length() != 1 {
        return operation_error("select expects three operands and one result")
      }
      if operands[0] != I32 ||
        operands[1] != operands[2] ||
        operands[1] != results[0] {
        return operation_error(
          "select expects i32 condition and matching value/result types",
        )
      }
      None
    }
    GcRefAddress =>
      require_shape(operands, results, [GcRef64], [Ptr64], "gcref.address")
    GcRefFromBits =>
      require_shape(operands, results, [I64], [GcRef64], "gcref.from_bits")
    PointerOffset =>
      require_shape(operands, results, [Ptr64, I64], [Ptr64], "pointer.offset")
    ReferenceCompare(_) => {
      if operands.length() != 2 ||
        results != [I32] ||
        operands[0] != operands[1] ||
        (operands[0] != Ptr64 && operands[0] != GcRef64) {
        return operation_error(
          "reference comparison expects matching ptr64 or gcref64 operands and i32 result",
        )
      }
      None
    }
    IntUnary(_) => {
      if operands.length() != 1 ||
        results.length() != 1 ||
        !is_integer_type(operands[0]) ||
        operands[0] != results[0] {
        return operation_error(
          "integer unary operation expects one matching i32 or i64 result",
        )
      }
      None
    }
    IntBinary(_) => {
      if operands.length() != 2 ||
        results.length() != 1 ||
        !is_integer_type(operands[0]) ||
        operands[0] != operands[1] ||
        operands[0] != results[0] {
        return operation_error(
          "integer binary operation expects matching i32 or i64 values",
        )
      }
      None
    }
    IntBinaryImmediate(_, _) => {
      if operands.length() != 1 ||
        results.length() != 1 ||
        !is_integer_type(operands[0]) ||
        operands[0] != results[0] {
        return operation_error(
          "integer immediate operation expects one matching i32 or i64 result",
        )
      }
      None
    }
    IntShiftImmediate(operation, amount) => {
      if operation != ShiftLeft &&
        operation != SignedShiftRight &&
        operation != UnsignedShiftRight &&
        operation != RotateLeft &&
        operation != RotateRight {
        return operation_error(
          "integer shift immediate requires a shift operation",
        )
      }
      if operands.length() != 1 ||
        results.length() != 1 ||
        !is_integer_type(operands[0]) ||
        operands[0] != results[0] {
        return operation_error(
          "integer shift immediate expects one matching i32 or i64 result",
        )
      }
      let width = value_type_bits(operands[0])
      if amount < 0 || amount >= width {
        return operation_error("integer shift immediate amount is out of range")
      }
      None
    }
    IntMultiplyAdd => {
      if operands.length() != 3 ||
        results.length() != 1 ||
        !is_integer_type(operands[0]) ||
        operands[0] != operands[1] ||
        operands[0] != operands[2] ||
        operands[0] != results[0] {
        return operation_error(
          "integer multiply-add expects three matching i32 or i64 operands",
        )
      }
      None
    }
    IntAddShiftedLeft(amount) => {
      if operands.length() != 2 ||
        results.length() != 1 ||
        !is_integer_type(operands[0]) ||
        operands[0] != operands[1] ||
        operands[0] != results[0] {
        return operation_error(
          "shifted integer add expects two matching i32 or i64 operands",
        )
      }
      let width = value_type_bits(operands[0])
      if amount < 0 || amount >= width {
        return operation_error("shifted integer add amount is out of range")
      }
      None
    }
    IntHighMultiply(_) => {
      if operands.length() != 2 ||
        results.length() != 1 ||
        !is_integer_type(operands[0]) ||
        operands[0] != operands[1] ||
        operands[0] != results[0] {
        return operation_error(
          "high-half multiply expects matching i32 or i64 values",
        )
      }
      None
    }
    IntWithOverflow(_) => {
      if operands.length() != 2 ||
        results.length() != 2 ||
        !is_integer_type(operands[0]) ||
        operands[0] != operands[1] ||
        results[0] != operands[0] ||
        results[1] != I32 {
        return operation_error(
          "integer overflow operation expects matching integer operands and [integer, i32] results",
        )
      }
      None
    }
    IntCompare(_) => {
      if operands.length() != 2 ||
        results != [I32] ||
        !is_integer_type(operands[0]) ||
        operands[0] != operands[1] {
        return operation_error(
          "integer comparison expects matching i32 or i64 operands and i32 result",
        )
      }
      None
    }
    FloatUnary(_) => {
      if operands.length() != 1 ||
        results.length() != 1 ||
        !is_float_type(operands[0]) ||
        operands[0] != results[0] {
        return operation_error(
          "float unary operation expects one matching f32 or f64 result",
        )
      }
      None
    }
    FloatBinary(_) => {
      if operands.length() != 2 ||
        results.length() != 1 ||
        !is_float_type(operands[0]) ||
        operands[0] != operands[1] ||
        operands[0] != results[0] {
        return operation_error(
          "float binary operation expects matching f32 or f64 values",
        )
      }
      None
    }
    FloatTernary(_) => {
      if operands.length() != 3 ||
        results.length() != 1 ||
        !is_float_type(operands[0]) ||
        operands[0] != operands[1] ||
        operands[0] != operands[2] ||
        operands[0] != results[0] {
        return operation_error(
          "float ternary operation expects matching f32 or f64 values",
        )
      }
      None
    }
    FloatCompare(_) => {
      if operands.length() != 2 ||
        results != [I32] ||
        !is_float_type(operands[0]) ||
        operands[0] != operands[1] {
        return operation_error(
          "float comparison expects matching f32 or f64 operands and i32 result",
        )
      }
      None
    }
    Convert(conversion) => {
      let expected : (Array[@native.ValueType], Array[@native.ValueType]) = match
        conversion {
        I32WrapI64 => ([I64], [I32])
        I64ExtendI32(_) => ([I32], [I64])
        F32DemoteF64 => ([F64], [F32])
        F64PromoteF32 => ([F32], [F64])
        FloatToInt(from, to, _, _) =>
          ([float_value_type(from)], [integer_value_type(to)])
        IntToFloat(from, to, _) =>
          ([integer_value_type(from)], [float_value_type(to)])
        SignExtend(integer_type, width) => {
          let ty = integer_value_type(integer_type)
          if width_bits(width) >= value_type_bits(ty) || width == W128 {
            return operation_error(
              "sign extension source width must be narrower than its integer value type",
            )
          }
          ([ty], [ty])
        }
        Bitcast(from, to) => {
          if value_type_bits(from) != value_type_bits(to) ||
            from == GcRef64 ||
            to == GcRef64 {
            return operation_error(
              "bitcast requires equal-width non-GC value types",
            )
          }
          ([from], [to])
        }
      }
      require_shape(operands, results, expected.0, expected.1, "conversion")
    }
    Load(spec) =>
      match verify_load_spec(spec) {
        Some(error) => Some(error)
        None =>
          require_shape(operands, results, [Ptr64], [spec.result_type], "load")
      }
    LoadIndexed(spec, shift) =>
      match verify_load_spec(spec) {
        Some(error) => Some(error)
        None if shift < 0 || shift > 4 =>
          operation_error("indexed load scale must be between 0 and 4")
        None =>
          require_shape(
            operands,
            results,
            [Ptr64, I32],
            [spec.result_type],
            "indexed load",
          )
      }
    Store(spec) =>
      match verify_store_spec(spec) {
        Some(error) => Some(error)
        None =>
          require_shape(
            operands,
            results,
            [Ptr64, spec.value_type],
            [],
            "store",
          )
      }
    StoreIndexed(spec, shift) =>
      match verify_store_spec(spec) {
        Some(error) => Some(error)
        None if shift < 0 || shift > 4 =>
          operation_error("indexed store scale must be between 0 and 4")
        None =>
          require_shape(
            operands,
            results,
            [Ptr64, I32, spec.value_type],
            [],
            "indexed store",
          )
      }
    AtomicLoad(spec) =>
      match verify_atomic_spec(spec) {
        Some(error) => Some(error)
        None =>
          require_shape(
            operands,
            results,
            [Ptr64],
            [spec.value_type],
            "atomic.load",
          )
      }
    AtomicStore(spec) =>
      match verify_atomic_spec(spec) {
        Some(error) => Some(error)
        None =>
          require_shape(
            operands,
            results,
            [Ptr64, spec.value_type],
            [],
            "atomic.store",
          )
      }
    AtomicRmw(spec, _) =>
      match verify_atomic_spec(spec) {
        Some(error) => Some(error)
        None =>
          require_shape(
            operands,
            results,
            [Ptr64, spec.value_type],
            [spec.value_type],
            "atomic.rmw",
          )
      }
    AtomicCompareExchange(spec) =>
      match verify_atomic_spec(spec) {
        Some(error) => Some(error)
        None =>
          require_shape(
            operands,
            results,
            [Ptr64, spec.value_type, spec.value_type],
            [spec.value_type],
            "atomic.compare_exchange",
          )
      }
    AtomicFence => require_shape(operands, results, [], [], "atomic.fence")
    Vector(vector_op) => verify_vector_operation(vector_op, operands, results)
    VectorLoad(spec) =>
      match verify_vector_load_spec(spec) {
        Some(error) => Some(error)
        None => {
          let expected_operands = match spec.kind {
            Lane(_, _) => [@native.Ptr64, V128]
            Splat(_) | Extend(_, _) | Zero(_) => [Ptr64]
          }
          require_shape(
            operands,
            results,
            expected_operands,
            [V128],
            "vector.load",
          )
        }
      }
    VectorStoreLane(spec) =>
      match verify_vector_store_lane_spec(spec) {
        Some(error) => Some(error)
        None =>
          require_shape(
            operands,
            results,
            [Ptr64, V128],
            [],
            "vector.store_lane",
          )
      }
    Call(call) =>
      match verify_call_operands(call, operands, "call") {
        Some(error) => Some(error)
        None =>
          if results != call.signature.results {
            operation_error(
              "call expects results \{Repr(call.signature.results)}, got \{Repr(results)}",
            )
          } else {
            None
          }
      }
    Safepoint(_) => require_shape(operands, results, [], [], "safepoint")
  }
}

///|
pub fn Operation::semantics(self : Operation) -> @native.OperationSemantics {
  match self {
    IntBinary(SignedDiv | UnsignedDiv | SignedRem | UnsignedRem) =>
      { ..@native.OperationSemantics::pure(), may_trap: true, }
    Convert(FloatToInt(_, _, _, Trapping)) =>
      { ..@native.OperationSemantics::pure(), may_trap: true, }
    Load(spec) =>
      {
        ..@native.OperationSemantics::pure(),
        memory: Read,
        may_trap: spec.trap is Some(_),
      }
    LoadIndexed(spec, _) =>
      {
        ..@native.OperationSemantics::pure(),
        memory: Read,
        may_trap: spec.trap is Some(_),
      }
    Store(spec) =>
      {
        ..@native.OperationSemantics::pure(),
        memory: Write,
        may_trap: spec.trap is Some(_),
      }
    StoreIndexed(spec, _) =>
      {
        ..@native.OperationSemantics::pure(),
        memory: Write,
        may_trap: spec.trap is Some(_),
      }
    AtomicLoad(spec) =>
      {
        ..@native.OperationSemantics::pure(),
        memory: Read,
        may_trap: spec.trap is Some(_),
      }
    AtomicStore(spec) =>
      {
        ..@native.OperationSemantics::pure(),
        memory: Write,
        may_trap: spec.trap is Some(_),
      }
    AtomicRmw(spec, _) | AtomicCompareExchange(spec) =>
      {
        ..@native.OperationSemantics::pure(),
        memory: ReadWrite,
        may_trap: spec.trap is Some(_),
      }
    AtomicFence => { ..@native.OperationSemantics::pure(), memory: ReadWrite, }
    VectorLoad(spec) =>
      {
        ..@native.OperationSemantics::pure(),
        memory: Read,
        may_trap: spec.trap is Some(_),
      }
    VectorStoreLane(spec) =>
      {
        ..@native.OperationSemantics::pure(),
        memory: Write,
        may_trap: spec.trap is Some(_),
      }
    EnvironmentField(_, _) =>
      { ..@native.OperationSemantics::pure(), memory: Read, }
    Call(call) => call.behavior.semantics()
    Safepoint(Gc) =>
      { ..@native.OperationSemantics::pure(), gc_safepoint: true, }
    Safepoint(Cancellation) =>
      { ..@native.OperationSemantics::pure(), cancellation_safepoint: true, }
    Safepoint(GcAndCancellation) =>
      {
        ..@native.OperationSemantics::pure(),
        gc_safepoint: true,
        cancellation_safepoint: true,
      }
    I32Const(_)
    | I64Const(_)
    | F32Const(_)
    | F64Const(_)
    | V128Const(_, _)
    | NullPtr
    | NullGcRef
    | CodeAddress(_)
    | ExternalAddress(_)
    | DataAddress(_)
    | StackAddress(_)
    | Copy
    | Select
    | GcRefAddress
    | GcRefFromBits
    | PointerOffset
    | ReferenceCompare(_)
    | IntUnary(_)
    | IntBinary(_)
    | IntBinaryImmediate(_, _)
    | IntShiftImmediate(_, _)
    | IntMultiplyAdd
    | IntAddShiftedLeft(_)
    | IntHighMultiply(_)
    | IntWithOverflow(_)
    | IntCompare(_)
    | FloatUnary(_)
    | FloatBinary(_)
    | FloatTernary(_)
    | FloatCompare(_)
    | Convert(_)
    | Vector(_) => @native.OperationSemantics::pure()
  }
}