Ops.cpp.inc

Go to the documentation of this file.

/*===- TableGen'erated file -------------------------------------*- C++ -*-===*\
|*                                                                            *|
|* Op Definitions                                                             *|
|*                                                                            *|
|* Automatically generated file, do not edit!                                 *|
|* From: Ops.td                                                               *|
|*                                                                            *|
\*===----------------------------------------------------------------------===*/
 
#ifdef GET_OP_LIST
#undef GET_OP_LIST
 
::llzk::verif::AssumeDetOp,
::llzk::verif::ContractEndOp,
::llzk::verif::ContractOp,
::llzk::verif::DecreasesOp,
::llzk::verif::EnsureComputeOp,
::llzk::verif::EnsureConstrainOp,
::llzk::verif::IncludeOp,
::llzk::verif::IncreasesOp,
::llzk::verif::InvariantOp,
::llzk::verif::OldOp,
::llzk::verif::ProveDetOp,
::llzk::verif::RequireComputeOp,
::llzk::verif::RequireConstrainOp,
::llzk::verif::StepOp,
::llzk::verif::StepYieldOp,
::llzk::verif::VerifAssertOp,
::llzk::verif::VerifProveOp,
::llzk::verif::VerifSMTProveOp
#endif // GET_OP_LIST
 
#ifdef GET_OP_CLASSES
#undef GET_OP_CLASSES
 
 
//===----------------------------------------------------------------------===//
// Local Utility Method Definitions
//===----------------------------------------------------------------------===//
 
 
static ::llvm::LogicalResult __mlir_ods_local_type_constraint_Ops1(
    ::mlir::Operation *op, ::mlir::Type type, ::llvm::StringRef valueKind,
    unsigned valueIndex) {
  if (!((::llzk::isValidEmitEqType(type)))) {
    return op->emitOpError(valueKind) << " #" << valueIndex
        << " must be any LLZK type, excluding struct and string types, but got " << type;
  }
  return ::mlir::success();
}
 
static ::llvm::LogicalResult __mlir_ods_local_type_constraint_Ops2(
    ::mlir::Operation *op, ::mlir::Type type, ::llvm::StringRef valueKind,
    unsigned valueIndex) {
  if (!((::llvm::isa<::llzk::felt::FeltType>(type)))) {
    return op->emitOpError(valueKind) << " #" << valueIndex
        << " must be finite field element, but got " << type;
  }
  return ::mlir::success();
}
 
static ::llvm::LogicalResult __mlir_ods_local_type_constraint_Ops3(
    ::mlir::Operation *op, ::mlir::Type type, ::llvm::StringRef valueKind,
    unsigned valueIndex) {
  if (!((type.isSignlessInteger(1)))) {
    return op->emitOpError(valueKind) << " #" << valueIndex
        << " must be 1-bit signless integer, but got " << type;
  }
  return ::mlir::success();
}
 
static ::llvm::LogicalResult __mlir_ods_local_type_constraint_Ops4(
    ::mlir::Operation *op, ::mlir::Type type, ::llvm::StringRef valueKind,
    unsigned valueIndex) {
  if (!((::llzk::isValidType(type)))) {
    return op->emitOpError(valueKind) << " #" << valueIndex
        << " must be variadic of a valid LLZK type, but got " << type;
  }
  return ::mlir::success();
}
 
static ::llvm::LogicalResult __mlir_ods_local_type_constraint_Ops5(
    ::mlir::Operation *op, ::mlir::Type type, ::llvm::StringRef valueKind,
    unsigned valueIndex) {
  if (!((::llvm::isa<::mlir::IndexType>(type)))) {
    return op->emitOpError(valueKind) << " #" << valueIndex
        << " must be variadic of index, but got " << type;
  }
  return ::mlir::success();
}
 
static ::llvm::LogicalResult __mlir_ods_local_type_constraint_Ops6(
    ::mlir::Operation *op, ::mlir::Type type, ::llvm::StringRef valueKind,
    unsigned valueIndex) {
  if (!((::llzk::isValidType(type)))) {
    return op->emitOpError(valueKind) << " #" << valueIndex
        << " must be a valid LLZK type, but got " << type;
  }
  return ::mlir::success();
}
 
static ::llvm::LogicalResult __mlir_ods_local_type_constraint_Ops7(
    ::mlir::Operation *op, ::mlir::Type type, ::llvm::StringRef valueKind,
    unsigned valueIndex) {
  if (!((::llvm::isa<mlir::smt::BoolType>(type)))) {
    return op->emitOpError(valueKind) << " #" << valueIndex
        << " must be , but got " << type;
  }
  return ::mlir::success();
}
 
static ::llvm::LogicalResult __mlir_ods_local_attr_constraint_Ops1(
    ::mlir::Attribute attr, ::llvm::StringRef attrName, llvm::function_ref<::mlir::InFlightDiagnostic()> emitError) {
  if (attr && !((::llvm::isa<::mlir::StringAttr>(attr))))
    return emitError() << "attribute '" << attrName
        << "' failed to satisfy constraint: string attribute";
  return ::mlir::success();
}
static ::llvm::LogicalResult __mlir_ods_local_attr_constraint_Ops1(
    ::mlir::Operation *op, ::mlir::Attribute attr, ::llvm::StringRef attrName) {
  return __mlir_ods_local_attr_constraint_Ops1(attr, attrName, [op]() {
    return op->emitOpError();
  });
}
 
static ::llvm::LogicalResult __mlir_ods_local_attr_constraint_Ops2(
    ::mlir::Attribute attr, ::llvm::StringRef attrName, llvm::function_ref<::mlir::InFlightDiagnostic()> emitError) {
  if (attr && !((::llvm::isa<::mlir::SymbolRefAttr>(attr))))
    return emitError() << "attribute '" << attrName
        << "' failed to satisfy constraint: symbol reference attribute";
  return ::mlir::success();
}
static ::llvm::LogicalResult __mlir_ods_local_attr_constraint_Ops2(
    ::mlir::Operation *op, ::mlir::Attribute attr, ::llvm::StringRef attrName) {
  return __mlir_ods_local_attr_constraint_Ops2(attr, attrName, [op]() {
    return op->emitOpError();
  });
}
 
static ::llvm::LogicalResult __mlir_ods_local_attr_constraint_Ops3(
    ::mlir::Attribute attr, ::llvm::StringRef attrName, llvm::function_ref<::mlir::InFlightDiagnostic()> emitError) {
  if (attr && !(((::llvm::isa<::mlir::TypeAttr>(attr))) && ((::llvm::isa<::mlir::FunctionType>(::llvm::cast<::mlir::TypeAttr>(attr).getValue()))) && ((::llvm::isa<::mlir::FunctionType>(::llvm::cast<::mlir::TypeAttr>(attr).getValue())))))
    return emitError() << "attribute '" << attrName
        << "' failed to satisfy constraint: type attribute of function type";
  return ::mlir::success();
}
static ::llvm::LogicalResult __mlir_ods_local_attr_constraint_Ops3(
    ::mlir::Operation *op, ::mlir::Attribute attr, ::llvm::StringRef attrName) {
  return __mlir_ods_local_attr_constraint_Ops3(attr, attrName, [op]() {
    return op->emitOpError();
  });
}
 
static ::llvm::LogicalResult __mlir_ods_local_attr_constraint_Ops4(
    ::mlir::Attribute attr, ::llvm::StringRef attrName, llvm::function_ref<::mlir::InFlightDiagnostic()> emitError) {
  if (attr && !(((::llvm::isa<::mlir::ArrayAttr>(attr))) && (::llvm::all_of(::llvm::cast<::mlir::ArrayAttr>(attr), [&](::mlir::Attribute attr) { return attr && ((::llvm::isa<::mlir::DictionaryAttr>(attr))); }))))
    return emitError() << "attribute '" << attrName
        << "' failed to satisfy constraint: Array of dictionary attributes";
  return ::mlir::success();
}
static ::llvm::LogicalResult __mlir_ods_local_attr_constraint_Ops4(
    ::mlir::Operation *op, ::mlir::Attribute attr, ::llvm::StringRef attrName) {
  return __mlir_ods_local_attr_constraint_Ops4(attr, attrName, [op]() {
    return op->emitOpError();
  });
}
 
static ::llvm::LogicalResult __mlir_ods_local_attr_constraint_Ops5(
    ::mlir::Attribute attr, ::llvm::StringRef attrName, llvm::function_ref<::mlir::InFlightDiagnostic()> emitError) {
  if (attr && !((::llvm::isa<::mlir::ArrayAttr>(attr))))
    return emitError() << "attribute '" << attrName
        << "' failed to satisfy constraint: array attribute";
  return ::mlir::success();
}
static ::llvm::LogicalResult __mlir_ods_local_attr_constraint_Ops5(
    ::mlir::Operation *op, ::mlir::Attribute attr, ::llvm::StringRef attrName) {
  return __mlir_ods_local_attr_constraint_Ops5(attr, attrName, [op]() {
    return op->emitOpError();
  });
}
 
static ::llvm::LogicalResult __mlir_ods_local_attr_constraint_Ops6(
    ::mlir::Attribute attr, ::llvm::StringRef attrName, llvm::function_ref<::mlir::InFlightDiagnostic()> emitError) {
  if (attr && !((::llvm::isa<::mlir::DenseI32ArrayAttr>(attr))))
    return emitError() << "attribute '" << attrName
        << "' failed to satisfy constraint: i32 dense array attribute";
  return ::mlir::success();
}
static ::llvm::LogicalResult __mlir_ods_local_attr_constraint_Ops6(
    ::mlir::Operation *op, ::mlir::Attribute attr, ::llvm::StringRef attrName) {
  return __mlir_ods_local_attr_constraint_Ops6(attr, attrName, [op]() {
    return op->emitOpError();
  });
}
 
static ::llvm::LogicalResult __mlir_ods_local_attr_constraint_Ops7(
    ::mlir::Attribute attr, ::llvm::StringRef attrName, llvm::function_ref<::mlir::InFlightDiagnostic()> emitError) {
  if (attr && !(((::llvm::isa<::mlir::ArrayAttr>(attr))) && (::llvm::all_of(::llvm::cast<::mlir::ArrayAttr>(attr), [&](::mlir::Attribute attr) { return attr && (((::llvm::isa<::mlir::TypeAttr>(attr))) && ((::llvm::isa<::mlir::Type>(::llvm::cast<::mlir::TypeAttr>(attr).getValue()))) && ((true))); }))))
    return emitError() << "attribute '" << attrName
        << "' failed to satisfy constraint: type array attribute";
  return ::mlir::success();
}
static ::llvm::LogicalResult __mlir_ods_local_attr_constraint_Ops7(
    ::mlir::Operation *op, ::mlir::Attribute attr, ::llvm::StringRef attrName) {
  return __mlir_ods_local_attr_constraint_Ops7(attr, attrName, [op]() {
    return op->emitOpError();
  });
}
 
static ::llvm::LogicalResult __mlir_ods_local_region_constraint_Ops1(
    ::mlir::Operation *op, ::mlir::Region &region, ::llvm::StringRef regionName,
    unsigned regionIndex) {
  if (!((true))) {
    return op->emitOpError("region #") << regionIndex
        << (regionName.empty() ? " " : " ('" + regionName + "') ")
        << "failed to verify constraint: any region";
  }
  return ::mlir::success();
}
 
static ::llvm::LogicalResult __mlir_ods_local_region_constraint_Ops2(
    ::mlir::Operation *op, ::mlir::Region &region, ::llvm::StringRef regionName,
    unsigned regionIndex) {
  if (!((::llvm::hasNItems(region, 1)))) {
    return op->emitOpError("region #") << regionIndex
        << (regionName.empty() ? " " : " ('" + regionName + "') ")
        << "failed to verify constraint: region with 1 blocks";
  }
  return ::mlir::success();
}
namespace llzk::verif {
 
 
//===----------------------------------------------------------------------===//
// ::llzk::verif::AssumeDetOp definitions
//===----------------------------------------------------------------------===//
 
namespace detail {
 
AssumeDetOpGenericAdaptorBase::AssumeDetOpGenericAdaptorBase(AssumeDetOp op) : odsAttrs(op->getRawDictionaryAttrs()), odsOpName(op->getName()), properties(op.getProperties()), odsRegions(op->getRegions()) {}
 
 
} // namespace detail
AssumeDetOpAdaptor::AssumeDetOpAdaptor(AssumeDetOp op) : AssumeDetOpGenericAdaptor(op->getOperands(), op) {}
 
::llvm::LogicalResult AssumeDetOpAdaptor::verify(::mlir::Location loc) {
  return ::mlir::success();
}
 
::llvm::LogicalResult AssumeDetOp::setPropertiesFromAttr(Properties &prop, ::mlir::Attribute attr, ::llvm::function_ref<::mlir::InFlightDiagnostic()> emitError) {
  ::mlir::DictionaryAttr dict = ::llvm::dyn_cast<::mlir::DictionaryAttr>(attr);
  if (!dict) {
    emitError() << "expected DictionaryAttr to set properties";
    return ::mlir::failure();
  }
      return ::mlir::success();
}
 
::mlir::Attribute AssumeDetOp::getPropertiesAsAttr(::mlir::MLIRContext *ctx, const Properties &prop) {
    ::mlir::SmallVector<::mlir::NamedAttribute> attrs;
    ::mlir::Builder odsBuilder{ctx};
 
  if (!attrs.empty())
    return odsBuilder.getDictionaryAttr(attrs);
  return {};
}
 
llvm::hash_code AssumeDetOp::computePropertiesHash(const Properties &prop) {
  using llvm::hash_value;
  return llvm::hash_combine();
}
 
std::optional<mlir::Attribute> AssumeDetOp::getInherentAttr(::mlir::MLIRContext *ctx, const Properties &prop, llvm::StringRef name) {
  return std::nullopt;
}
 
void AssumeDetOp::setInherentAttr(Properties &prop, llvm::StringRef name, mlir::Attribute value) {
}
 
void AssumeDetOp::populateInherentAttrs(::mlir::MLIRContext *ctx, const Properties &prop, ::mlir::NamedAttrList &attrs) {
}
 
::llvm::LogicalResult AssumeDetOp::verifyInherentAttrs(::mlir::OperationName opName, ::mlir::NamedAttrList &attrs, llvm::function_ref<::mlir::InFlightDiagnostic()> emitError) {
    return ::mlir::success();
}
 
void AssumeDetOp::build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, ::mlir::Value hint) {
  odsState.addOperands(hint);
}
 
AssumeDetOp AssumeDetOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::Value hint) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(hint)>(hint));
  auto __res__ = ::llvm::dyn_cast<AssumeDetOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
AssumeDetOp AssumeDetOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::Value hint) {
  return create(builder, builder.getLoc(), std::forward<decltype(hint)>(hint));
}
 
void AssumeDetOp::build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, ::mlir::TypeRange resultTypes, ::mlir::Value hint) {
  odsState.addOperands(hint);
  assert(resultTypes.size() == 0u && "mismatched number of results");
  odsState.addTypes(resultTypes);
}
 
AssumeDetOp AssumeDetOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::TypeRange resultTypes, ::mlir::Value hint) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(hint)>(hint));
  auto __res__ = ::llvm::dyn_cast<AssumeDetOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
AssumeDetOp AssumeDetOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::TypeRange resultTypes, ::mlir::Value hint) {
  return create(builder, builder.getLoc(), std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(hint)>(hint));
}
 
void AssumeDetOp::build(::mlir::OpBuilder &, ::mlir::OperationState &odsState, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, ::llvm::ArrayRef<::mlir::NamedAttribute> attributes) {
  assert(operands.size() == 1u && "mismatched number of parameters");
  odsState.addOperands(operands);
  odsState.addAttributes(attributes);
  assert(resultTypes.size() == 0u && "mismatched number of return types");
  odsState.addTypes(resultTypes);
}
 
AssumeDetOp AssumeDetOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, ::llvm::ArrayRef<::mlir::NamedAttribute> attributes) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(operands)>(operands), std::forward<decltype(attributes)>(attributes));
  auto __res__ = ::llvm::dyn_cast<AssumeDetOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
AssumeDetOp AssumeDetOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, ::llvm::ArrayRef<::mlir::NamedAttribute> attributes) {
  return create(builder, builder.getLoc(), std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(operands)>(operands), std::forward<decltype(attributes)>(attributes));
}
 
void AssumeDetOp::build(::mlir::OpBuilder &, ::mlir::OperationState &odsState, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, const Properties &properties, ::llvm::ArrayRef<::mlir::NamedAttribute> discardableAttributes) {
  assert(operands.size() == 1u && "mismatched number of parameters");
  odsState.addOperands(operands);
  odsState.useProperties(const_cast<Properties&>(properties));
  odsState.addAttributes(discardableAttributes);
  assert(resultTypes.size() == 0u && "mismatched number of return types");
  odsState.addTypes(resultTypes);
}
 
AssumeDetOp AssumeDetOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, const Properties &properties, ::llvm::ArrayRef<::mlir::NamedAttribute> discardableAttributes) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(operands)>(operands), std::forward<decltype(properties)>(properties), std::forward<decltype(discardableAttributes)>(discardableAttributes));
  auto __res__ = ::llvm::dyn_cast<AssumeDetOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
AssumeDetOp AssumeDetOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, const Properties &properties, ::llvm::ArrayRef<::mlir::NamedAttribute> discardableAttributes) {
  return create(builder, builder.getLoc(), std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(operands)>(operands), std::forward<decltype(properties)>(properties), std::forward<decltype(discardableAttributes)>(discardableAttributes));
}
 
::llvm::LogicalResult AssumeDetOp::verifyInvariantsImpl() {
  {
    unsigned index = 0; (void)index;
    auto valueGroup0 = getODSOperands(0);
 
    for (auto v : valueGroup0) {
      if (::mlir::failed(__mlir_ods_local_type_constraint_Ops1(*this, v.getType(), "operand", index++)))
        return ::mlir::failure();
    }
  }
  return ::mlir::success();
}
 
::llvm::LogicalResult AssumeDetOp::verifyInvariants() {
  return verifyInvariantsImpl();
}
 
::mlir::ParseResult AssumeDetOp::parse(::mlir::OpAsmParser &parser, ::mlir::OperationState &result) {
  ::mlir::OpAsmParser::UnresolvedOperand hintRawOperand{};
  ::llvm::ArrayRef<::mlir::OpAsmParser::UnresolvedOperand> hintOperands(&hintRawOperand, 1);  ::llvm::SMLoc hintOperandsLoc;
  (void)hintOperandsLoc;
  ::mlir::Type hintRawType{};
  ::llvm::ArrayRef<::mlir::Type> hintTypes(&hintRawType, 1);
 
  hintOperandsLoc = parser.getCurrentLocation();
  if (parser.parseOperand(hintRawOperand))
    return ::mlir::failure();
  {
    auto loc = parser.getCurrentLocation();(void)loc;
    if (parser.parseOptionalAttrDict(result.attributes))
      return ::mlir::failure();
    if (failed(verifyInherentAttrs(result.name, result.attributes, [&]() {
        return parser.emitError(loc) << "'" << result.name.getStringRef() << "' op ";
      })))
      return ::mlir::failure();
  }
  if (parser.parseColon())
    return ::mlir::failure();
 
  {
    ::mlir::Type type;
    if (parser.parseCustomTypeWithFallback(type))
      return ::mlir::failure();
    hintRawType = type;
  }
  if (parser.resolveOperands(hintOperands, hintTypes, hintOperandsLoc, result.operands))
    return ::mlir::failure();
  return ::mlir::success();
}
 
void AssumeDetOp::print(::mlir::OpAsmPrinter &_odsPrinter) {
  _odsPrinter << ' ';
  _odsPrinter << getHint();
  ::llvm::SmallVector<::llvm::StringRef, 2> elidedAttrs;
  _odsPrinter.printOptionalAttrDict((*this)->getAttrs(), elidedAttrs);
  _odsPrinter << ' ' << ":";
  _odsPrinter << ' ';
  {
    auto type = getHint().getType();
    if (auto validType = ::llvm::dyn_cast<::mlir::Type>(type))
      _odsPrinter.printStrippedAttrOrType(validType);
   else
     _odsPrinter << type;
  }
}
 
// This side effect models "program termination". Based on
// https://github.com/llvm/llvm-project/blob/f325e4b2d836d6e65a4d0cf3efc6b0996ccf3765/mlir/lib/Dialect/ControlFlow/IR/ControlFlowOps.cpp#L92-L97
static void getEffects(
    ::mlir::SmallVectorImpl<::mlir::SideEffects::EffectInstance<::mlir::MemoryEffects::Effect>> &effects
) {
  effects.emplace_back(::mlir::MemoryEffects::Write::get());
}
 
} // namespace llzk::verif
MLIR_DEFINE_EXPLICIT_TYPE_ID(::llzk::verif::AssumeDetOp)
 
namespace llzk::verif {
 
 
//===----------------------------------------------------------------------===//
// ::llzk::verif::ContractEndOp definitions
//===----------------------------------------------------------------------===//
 
namespace detail {
 
ContractEndOpGenericAdaptorBase::ContractEndOpGenericAdaptorBase(ContractEndOp op) : odsAttrs(op->getRawDictionaryAttrs()), odsOpName(op->getName()), properties(op.getProperties()), odsRegions(op->getRegions()) {}
 
 
} // namespace detail
ContractEndOpAdaptor::ContractEndOpAdaptor(ContractEndOp op) : ContractEndOpGenericAdaptor(op->getOperands(), op) {}
 
::llvm::LogicalResult ContractEndOpAdaptor::verify(::mlir::Location loc) {
  return ::mlir::success();
}
 
::llvm::LogicalResult ContractEndOp::setPropertiesFromAttr(Properties &prop, ::mlir::Attribute attr, ::llvm::function_ref<::mlir::InFlightDiagnostic()> emitError) {
  ::mlir::DictionaryAttr dict = ::llvm::dyn_cast<::mlir::DictionaryAttr>(attr);
  if (!dict) {
    emitError() << "expected DictionaryAttr to set properties";
    return ::mlir::failure();
  }
      return ::mlir::success();
}
 
::mlir::Attribute ContractEndOp::getPropertiesAsAttr(::mlir::MLIRContext *ctx, const Properties &prop) {
    ::mlir::SmallVector<::mlir::NamedAttribute> attrs;
    ::mlir::Builder odsBuilder{ctx};
 
  if (!attrs.empty())
    return odsBuilder.getDictionaryAttr(attrs);
  return {};
}
 
llvm::hash_code ContractEndOp::computePropertiesHash(const Properties &prop) {
  using llvm::hash_value;
  return llvm::hash_combine();
}
 
std::optional<mlir::Attribute> ContractEndOp::getInherentAttr(::mlir::MLIRContext *ctx, const Properties &prop, llvm::StringRef name) {
  return std::nullopt;
}
 
void ContractEndOp::setInherentAttr(Properties &prop, llvm::StringRef name, mlir::Attribute value) {
}
 
void ContractEndOp::populateInherentAttrs(::mlir::MLIRContext *ctx, const Properties &prop, ::mlir::NamedAttrList &attrs) {
}
 
::llvm::LogicalResult ContractEndOp::verifyInherentAttrs(::mlir::OperationName opName, ::mlir::NamedAttrList &attrs, llvm::function_ref<::mlir::InFlightDiagnostic()> emitError) {
    return ::mlir::success();
}
 
void ContractEndOp::build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState) {
}
 
ContractEndOp ContractEndOp::create(::mlir::OpBuilder &builder, ::mlir::Location location) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__);
  auto __res__ = ::llvm::dyn_cast<ContractEndOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
ContractEndOp ContractEndOp::create(::mlir::ImplicitLocOpBuilder &builder) {
  return create(builder, builder.getLoc());
}
 
void ContractEndOp::build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, ::mlir::TypeRange resultTypes) {
  assert(resultTypes.size() == 0u && "mismatched number of results");
  odsState.addTypes(resultTypes);
}
 
ContractEndOp ContractEndOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::TypeRange resultTypes) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(resultTypes)>(resultTypes));
  auto __res__ = ::llvm::dyn_cast<ContractEndOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
ContractEndOp ContractEndOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::TypeRange resultTypes) {
  return create(builder, builder.getLoc(), std::forward<decltype(resultTypes)>(resultTypes));
}
 
void ContractEndOp::build(::mlir::OpBuilder &, ::mlir::OperationState &odsState, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, ::llvm::ArrayRef<::mlir::NamedAttribute> attributes) {
  assert(operands.size() == 0u && "mismatched number of parameters");
  odsState.addOperands(operands);
  odsState.addAttributes(attributes);
  assert(resultTypes.size() == 0u && "mismatched number of return types");
  odsState.addTypes(resultTypes);
}
 
ContractEndOp ContractEndOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, ::llvm::ArrayRef<::mlir::NamedAttribute> attributes) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(operands)>(operands), std::forward<decltype(attributes)>(attributes));
  auto __res__ = ::llvm::dyn_cast<ContractEndOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
ContractEndOp ContractEndOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, ::llvm::ArrayRef<::mlir::NamedAttribute> attributes) {
  return create(builder, builder.getLoc(), std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(operands)>(operands), std::forward<decltype(attributes)>(attributes));
}
 
void ContractEndOp::build(::mlir::OpBuilder &, ::mlir::OperationState &odsState, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, const Properties &properties, ::llvm::ArrayRef<::mlir::NamedAttribute> discardableAttributes) {
  assert(operands.size() == 0u && "mismatched number of parameters");
  odsState.addOperands(operands);
  odsState.useProperties(const_cast<Properties&>(properties));
  odsState.addAttributes(discardableAttributes);
  assert(resultTypes.size() == 0u && "mismatched number of return types");
  odsState.addTypes(resultTypes);
}
 
ContractEndOp ContractEndOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, const Properties &properties, ::llvm::ArrayRef<::mlir::NamedAttribute> discardableAttributes) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(operands)>(operands), std::forward<decltype(properties)>(properties), std::forward<decltype(discardableAttributes)>(discardableAttributes));
  auto __res__ = ::llvm::dyn_cast<ContractEndOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
ContractEndOp ContractEndOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, const Properties &properties, ::llvm::ArrayRef<::mlir::NamedAttribute> discardableAttributes) {
  return create(builder, builder.getLoc(), std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(operands)>(operands), std::forward<decltype(properties)>(properties), std::forward<decltype(discardableAttributes)>(discardableAttributes));
}
 
::llvm::LogicalResult ContractEndOp::verifyInvariantsImpl() {
  return ::mlir::success();
}
 
::llvm::LogicalResult ContractEndOp::verifyInvariants() {
  return verifyInvariantsImpl();
}
 
::mlir::ParseResult ContractEndOp::parse(::mlir::OpAsmParser &parser, ::mlir::OperationState &result) {
  {
    auto loc = parser.getCurrentLocation();(void)loc;
    if (parser.parseOptionalAttrDict(result.attributes))
      return ::mlir::failure();
    if (failed(verifyInherentAttrs(result.name, result.attributes, [&]() {
        return parser.emitError(loc) << "'" << result.name.getStringRef() << "' op ";
      })))
      return ::mlir::failure();
  }
  return ::mlir::success();
}
 
void ContractEndOp::print(::mlir::OpAsmPrinter &_odsPrinter) {
  ::llvm::SmallVector<::llvm::StringRef, 2> elidedAttrs;
  _odsPrinter.printOptionalAttrDict((*this)->getAttrs(), elidedAttrs);
}
 
void ContractEndOp::getEffects(::llvm::SmallVectorImpl<::mlir::SideEffects::EffectInstance<::mlir::MemoryEffects::Effect>> &effects) {
}
 
 
} // namespace llzk::verif
MLIR_DEFINE_EXPLICIT_TYPE_ID(::llzk::verif::ContractEndOp)
 
namespace llzk::verif {
 
 
//===----------------------------------------------------------------------===//
// ::llzk::verif::ContractOp definitions
//===----------------------------------------------------------------------===//
 
namespace detail {
 
ContractOpGenericAdaptorBase::ContractOpGenericAdaptorBase(ContractOp op) : odsAttrs(op->getRawDictionaryAttrs()), odsOpName(op->getName()), properties(op.getProperties()), odsRegions(op->getRegions()) {}
 
::llvm::StringRef ContractOpGenericAdaptorBase::getSymName() {
  auto attr = getSymNameAttr();
  return attr.getValue();
}
 
::mlir::SymbolRefAttr ContractOpGenericAdaptorBase::getTarget() {
  auto attr = getTargetAttr();
  return attr;
}
 
::mlir::FunctionType ContractOpGenericAdaptorBase::getFunctionType() {
  auto attr = getFunctionTypeAttr();
  return ::llvm::cast<::mlir::FunctionType>(attr.getValue());
}
 
::std::optional< ::mlir::ArrayAttr > ContractOpGenericAdaptorBase::getArgAttrs() {
  auto attr = getArgAttrsAttr();
  return attr ? ::std::optional< ::mlir::ArrayAttr >(attr) : (::std::nullopt);
}
 
::std::optional< ::mlir::ArrayAttr > ContractOpGenericAdaptorBase::getResAttrs() {
  auto attr = getResAttrsAttr();
  return attr ? ::std::optional< ::mlir::ArrayAttr >(attr) : (::std::nullopt);
}
 
 
} // namespace detail
ContractOpAdaptor::ContractOpAdaptor(ContractOp op) : ContractOpGenericAdaptor(op->getOperands(), op) {}
 
::llvm::LogicalResult ContractOpAdaptor::verify(::mlir::Location loc) {
  auto tblgen_arg_attrs = getProperties().arg_attrs; (void)tblgen_arg_attrs;
  auto tblgen_function_type = getProperties().function_type; (void)tblgen_function_type;
  if (!tblgen_function_type) return emitError(loc, "'verif.contract' op requires attribute 'function_type'");
  auto tblgen_res_attrs = getProperties().res_attrs; (void)tblgen_res_attrs;
  auto tblgen_sym_name = getProperties().sym_name; (void)tblgen_sym_name;
  if (!tblgen_sym_name) return emitError(loc, "'verif.contract' op requires attribute 'sym_name'");
  auto tblgen_target = getProperties().target; (void)tblgen_target;
  if (!tblgen_target) return emitError(loc, "'verif.contract' op requires attribute 'target'");
 
  if (tblgen_sym_name && !((::llvm::isa<::mlir::StringAttr>(tblgen_sym_name))))
    return emitError(loc, "'verif.contract' op attribute 'sym_name' failed to satisfy constraint: string attribute");
 
  if (tblgen_target && !((::llvm::isa<::mlir::SymbolRefAttr>(tblgen_target))))
    return emitError(loc, "'verif.contract' op attribute 'target' failed to satisfy constraint: symbol reference attribute");
 
  if (tblgen_function_type && !(((::llvm::isa<::mlir::TypeAttr>(tblgen_function_type))) && ((::llvm::isa<::mlir::FunctionType>(::llvm::cast<::mlir::TypeAttr>(tblgen_function_type).getValue()))) && ((::llvm::isa<::mlir::FunctionType>(::llvm::cast<::mlir::TypeAttr>(tblgen_function_type).getValue())))))
    return emitError(loc, "'verif.contract' op attribute 'function_type' failed to satisfy constraint: type attribute of function type");
 
  if (tblgen_arg_attrs && !(((::llvm::isa<::mlir::ArrayAttr>(tblgen_arg_attrs))) && (::llvm::all_of(::llvm::cast<::mlir::ArrayAttr>(tblgen_arg_attrs), [&](::mlir::Attribute attr) { return attr && ((::llvm::isa<::mlir::DictionaryAttr>(attr))); }))))
    return emitError(loc, "'verif.contract' op attribute 'arg_attrs' failed to satisfy constraint: Array of dictionary attributes");
 
  if (tblgen_res_attrs && !(((::llvm::isa<::mlir::ArrayAttr>(tblgen_res_attrs))) && (::llvm::all_of(::llvm::cast<::mlir::ArrayAttr>(tblgen_res_attrs), [&](::mlir::Attribute attr) { return attr && ((::llvm::isa<::mlir::DictionaryAttr>(attr))); }))))
    return emitError(loc, "'verif.contract' op attribute 'res_attrs' failed to satisfy constraint: Array of dictionary attributes");
  return ::mlir::success();
}
 
::llvm::LogicalResult ContractOp::setPropertiesFromAttr(Properties &prop, ::mlir::Attribute attr, ::llvm::function_ref<::mlir::InFlightDiagnostic()> emitError) {
  ::mlir::DictionaryAttr dict = ::llvm::dyn_cast<::mlir::DictionaryAttr>(attr);
  if (!dict) {
    emitError() << "expected DictionaryAttr to set properties";
    return ::mlir::failure();
  }
 
  {
    auto &propStorage = prop.arg_attrs;
       auto attr = dict.get("arg_attrs");
    if (attr) {
      auto convertedAttr = ::llvm::dyn_cast<std::remove_reference_t<decltype(propStorage)>>(attr);
      if (convertedAttr) {
        propStorage = convertedAttr;
      } else {
        emitError() << "Invalid attribute `arg_attrs` in property conversion: " << attr;
        return ::mlir::failure();
      }
    }
  }
 
  {
    auto &propStorage = prop.function_type;
       auto attr = dict.get("function_type");
    if (attr) {
      auto convertedAttr = ::llvm::dyn_cast<std::remove_reference_t<decltype(propStorage)>>(attr);
      if (convertedAttr) {
        propStorage = convertedAttr;
      } else {
        emitError() << "Invalid attribute `function_type` in property conversion: " << attr;
        return ::mlir::failure();
      }
    }
  }
 
  {
    auto &propStorage = prop.res_attrs;
       auto attr = dict.get("res_attrs");
    if (attr) {
      auto convertedAttr = ::llvm::dyn_cast<std::remove_reference_t<decltype(propStorage)>>(attr);
      if (convertedAttr) {
        propStorage = convertedAttr;
      } else {
        emitError() << "Invalid attribute `res_attrs` in property conversion: " << attr;
        return ::mlir::failure();
      }
    }
  }
 
  {
    auto &propStorage = prop.sym_name;
       auto attr = dict.get("sym_name");
    if (attr) {
      auto convertedAttr = ::llvm::dyn_cast<std::remove_reference_t<decltype(propStorage)>>(attr);
      if (convertedAttr) {
        propStorage = convertedAttr;
      } else {
        emitError() << "Invalid attribute `sym_name` in property conversion: " << attr;
        return ::mlir::failure();
      }
    }
  }
 
  {
    auto &propStorage = prop.target;
       auto attr = dict.get("target");
    if (attr) {
      auto convertedAttr = ::llvm::dyn_cast<std::remove_reference_t<decltype(propStorage)>>(attr);
      if (convertedAttr) {
        propStorage = convertedAttr;
      } else {
        emitError() << "Invalid attribute `target` in property conversion: " << attr;
        return ::mlir::failure();
      }
    }
  }
  return ::mlir::success();
}
 
::mlir::Attribute ContractOp::getPropertiesAsAttr(::mlir::MLIRContext *ctx, const Properties &prop) {
    ::mlir::SmallVector<::mlir::NamedAttribute> attrs;
    ::mlir::Builder odsBuilder{ctx};
 
    {
      const auto &propStorage = prop.arg_attrs;
      if (propStorage)
        attrs.push_back(odsBuilder.getNamedAttr("arg_attrs",
                                       propStorage));
    }
 
    {
      const auto &propStorage = prop.function_type;
      if (propStorage)
        attrs.push_back(odsBuilder.getNamedAttr("function_type",
                                       propStorage));
    }
 
    {
      const auto &propStorage = prop.res_attrs;
      if (propStorage)
        attrs.push_back(odsBuilder.getNamedAttr("res_attrs",
                                       propStorage));
    }
 
    {
      const auto &propStorage = prop.sym_name;
      if (propStorage)
        attrs.push_back(odsBuilder.getNamedAttr("sym_name",
                                       propStorage));
    }
 
    {
      const auto &propStorage = prop.target;
      if (propStorage)
        attrs.push_back(odsBuilder.getNamedAttr("target",
                                       propStorage));
    }
 
  if (!attrs.empty())
    return odsBuilder.getDictionaryAttr(attrs);
  return {};
}
 
llvm::hash_code ContractOp::computePropertiesHash(const Properties &prop) {
  using llvm::hash_value;
  return llvm::hash_combine(
    llvm::hash_value(prop.arg_attrs.getAsOpaquePointer()), 
    llvm::hash_value(prop.function_type.getAsOpaquePointer()), 
    llvm::hash_value(prop.res_attrs.getAsOpaquePointer()), 
    llvm::hash_value(prop.sym_name.getAsOpaquePointer()), 
    llvm::hash_value(prop.target.getAsOpaquePointer()));
}
 
std::optional<mlir::Attribute> ContractOp::getInherentAttr(::mlir::MLIRContext *ctx, const Properties &prop, llvm::StringRef name) {
    if (name == "arg_attrs")
      return prop.arg_attrs;
 
    if (name == "function_type")
      return prop.function_type;
 
    if (name == "res_attrs")
      return prop.res_attrs;
 
    if (name == "sym_name")
      return prop.sym_name;
 
    if (name == "target")
      return prop.target;
  return std::nullopt;
}
 
void ContractOp::setInherentAttr(Properties &prop, llvm::StringRef name, mlir::Attribute value) {
    if (name == "arg_attrs") {
       prop.arg_attrs = ::llvm::dyn_cast_or_null<std::remove_reference_t<decltype(prop.arg_attrs)>>(value);
       return;
    }
 
    if (name == "function_type") {
       prop.function_type = ::llvm::dyn_cast_or_null<std::remove_reference_t<decltype(prop.function_type)>>(value);
       return;
    }
 
    if (name == "res_attrs") {
       prop.res_attrs = ::llvm::dyn_cast_or_null<std::remove_reference_t<decltype(prop.res_attrs)>>(value);
       return;
    }
 
    if (name == "sym_name") {
       prop.sym_name = ::llvm::dyn_cast_or_null<std::remove_reference_t<decltype(prop.sym_name)>>(value);
       return;
    }
 
    if (name == "target") {
       prop.target = ::llvm::dyn_cast_or_null<std::remove_reference_t<decltype(prop.target)>>(value);
       return;
    }
}
 
void ContractOp::populateInherentAttrs(::mlir::MLIRContext *ctx, const Properties &prop, ::mlir::NamedAttrList &attrs) {
    if (prop.arg_attrs) attrs.append("arg_attrs", prop.arg_attrs);
 
    if (prop.function_type) attrs.append("function_type", prop.function_type);
 
    if (prop.res_attrs) attrs.append("res_attrs", prop.res_attrs);
 
    if (prop.sym_name) attrs.append("sym_name", prop.sym_name);
 
    if (prop.target) attrs.append("target", prop.target);
}
 
::llvm::LogicalResult ContractOp::verifyInherentAttrs(::mlir::OperationName opName, ::mlir::NamedAttrList &attrs, llvm::function_ref<::mlir::InFlightDiagnostic()> emitError) {
    {
      ::mlir::Attribute attr = attrs.get(getArgAttrsAttrName(opName));
      if (attr && ::mlir::failed(__mlir_ods_local_attr_constraint_Ops4(attr, "arg_attrs", emitError)))
        return ::mlir::failure();
    }
 
    {
      ::mlir::Attribute attr = attrs.get(getFunctionTypeAttrName(opName));
      if (attr && ::mlir::failed(__mlir_ods_local_attr_constraint_Ops3(attr, "function_type", emitError)))
        return ::mlir::failure();
    }
 
    {
      ::mlir::Attribute attr = attrs.get(getResAttrsAttrName(opName));
      if (attr && ::mlir::failed(__mlir_ods_local_attr_constraint_Ops4(attr, "res_attrs", emitError)))
        return ::mlir::failure();
    }
 
    {
      ::mlir::Attribute attr = attrs.get(getSymNameAttrName(opName));
      if (attr && ::mlir::failed(__mlir_ods_local_attr_constraint_Ops1(attr, "sym_name", emitError)))
        return ::mlir::failure();
    }
 
    {
      ::mlir::Attribute attr = attrs.get(getTargetAttrName(opName));
      if (attr && ::mlir::failed(__mlir_ods_local_attr_constraint_Ops2(attr, "target", emitError)))
        return ::mlir::failure();
    }
    return ::mlir::success();
}
 
::llvm::LogicalResult ContractOp::readProperties(::mlir::DialectBytecodeReader &reader, ::mlir::OperationState &state) {
  auto &prop = state.getOrAddProperties<Properties>(); (void)prop;
  if (::mlir::failed(reader.readOptionalAttribute(prop.arg_attrs)))
    return ::mlir::failure();
 
  if (::mlir::failed(reader.readAttribute(prop.function_type)))
    return ::mlir::failure();
 
  if (::mlir::failed(reader.readOptionalAttribute(prop.res_attrs)))
    return ::mlir::failure();
 
  if (::mlir::failed(reader.readAttribute(prop.sym_name)))
    return ::mlir::failure();
 
  if (::mlir::failed(reader.readAttribute(prop.target)))
    return ::mlir::failure();
  return ::mlir::success();
}
 
void ContractOp::writeProperties(::mlir::DialectBytecodeWriter &writer) {
  auto &prop = getProperties(); (void)prop;
 
  writer.writeOptionalAttribute(prop.arg_attrs);
  writer.writeAttribute(prop.function_type);
 
  writer.writeOptionalAttribute(prop.res_attrs);
  writer.writeAttribute(prop.sym_name);
  writer.writeAttribute(prop.target);
}
 
::llvm::StringRef ContractOp::getSymName() {
  auto attr = getSymNameAttr();
  return attr.getValue();
}
 
::mlir::SymbolRefAttr ContractOp::getTarget() {
  auto attr = getTargetAttr();
  return attr;
}
 
::mlir::FunctionType ContractOp::getFunctionType() {
  auto attr = getFunctionTypeAttr();
  return ::llvm::cast<::mlir::FunctionType>(attr.getValue());
}
 
::std::optional< ::mlir::ArrayAttr > ContractOp::getArgAttrs() {
  auto attr = getArgAttrsAttr();
  return attr ? ::std::optional< ::mlir::ArrayAttr >(attr) : (::std::nullopt);
}
 
::std::optional< ::mlir::ArrayAttr > ContractOp::getResAttrs() {
  auto attr = getResAttrsAttr();
  return attr ? ::std::optional< ::mlir::ArrayAttr >(attr) : (::std::nullopt);
}
 
void ContractOp::setSymName(::llvm::StringRef attrValue) {
  getProperties().sym_name = ::mlir::Builder((*this)->getContext()).getStringAttr(attrValue);
}
 
void ContractOp::setFunctionType(::mlir::FunctionType attrValue) {
  getProperties().function_type = ::mlir::TypeAttr::get(attrValue);
}
 
void ContractOp::build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, ::mlir::StringAttr sym_name, ::mlir::SymbolRefAttr target, ::mlir::TypeAttr function_type, ::mlir::ArrayAttr arg_attrs, ::mlir::ArrayAttr res_attrs) {
        build(odsBuilder, odsState, ::mlir::TypeRange {}, sym_name, target, function_type, arg_attrs,
              res_attrs);
      
}
 
ContractOp ContractOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::StringAttr sym_name, ::mlir::SymbolRefAttr target, ::mlir::TypeAttr function_type, ::mlir::ArrayAttr arg_attrs, ::mlir::ArrayAttr res_attrs) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(sym_name)>(sym_name), std::forward<decltype(target)>(target), std::forward<decltype(function_type)>(function_type), std::forward<decltype(arg_attrs)>(arg_attrs), std::forward<decltype(res_attrs)>(res_attrs));
  auto __res__ = ::llvm::dyn_cast<ContractOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
ContractOp ContractOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::StringAttr sym_name, ::mlir::SymbolRefAttr target, ::mlir::TypeAttr function_type, ::mlir::ArrayAttr arg_attrs, ::mlir::ArrayAttr res_attrs) {
  return create(builder, builder.getLoc(), std::forward<decltype(sym_name)>(sym_name), std::forward<decltype(target)>(target), std::forward<decltype(function_type)>(function_type), std::forward<decltype(arg_attrs)>(arg_attrs), std::forward<decltype(res_attrs)>(res_attrs));
}
 
void ContractOp::build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, ::mlir::TypeRange resultTypes, ::mlir::StringAttr sym_name, ::mlir::SymbolRefAttr target, ::mlir::TypeAttr function_type, ::mlir::ArrayAttr arg_attrs, ::mlir::ArrayAttr res_attrs) {
        odsState.getOrAddProperties<Properties>().sym_name = sym_name;
        odsState.getOrAddProperties<Properties>().target = target;
        odsState.getOrAddProperties<Properties>().function_type = function_type;
        if (arg_attrs) {
          odsState.getOrAddProperties<Properties>().arg_attrs = arg_attrs;
        }
        if (res_attrs) {
          odsState.getOrAddProperties<Properties>().res_attrs = res_attrs;
        }
        initializeEmptyBody(
            odsBuilder, odsState, ::llvm::cast<::mlir::FunctionType>(function_type.getValue())
        );
        assert(resultTypes.size() == 0u && "mismatched number of results");
        odsState.addTypes(resultTypes);
      
}
 
ContractOp ContractOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::TypeRange resultTypes, ::mlir::StringAttr sym_name, ::mlir::SymbolRefAttr target, ::mlir::TypeAttr function_type, ::mlir::ArrayAttr arg_attrs, ::mlir::ArrayAttr res_attrs) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(sym_name)>(sym_name), std::forward<decltype(target)>(target), std::forward<decltype(function_type)>(function_type), std::forward<decltype(arg_attrs)>(arg_attrs), std::forward<decltype(res_attrs)>(res_attrs));
  auto __res__ = ::llvm::dyn_cast<ContractOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
ContractOp ContractOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::TypeRange resultTypes, ::mlir::StringAttr sym_name, ::mlir::SymbolRefAttr target, ::mlir::TypeAttr function_type, ::mlir::ArrayAttr arg_attrs, ::mlir::ArrayAttr res_attrs) {
  return create(builder, builder.getLoc(), std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(sym_name)>(sym_name), std::forward<decltype(target)>(target), std::forward<decltype(function_type)>(function_type), std::forward<decltype(arg_attrs)>(arg_attrs), std::forward<decltype(res_attrs)>(res_attrs));
}
 
void ContractOp::build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, ::llvm::StringRef sym_name, ::mlir::SymbolRefAttr target, ::mlir::FunctionType function_type, ::mlir::ArrayAttr arg_attrs, ::mlir::ArrayAttr res_attrs) {
        build(odsBuilder, odsState, ::mlir::TypeRange {}, sym_name, target, function_type, arg_attrs,
              res_attrs);
      
}
 
ContractOp ContractOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::llvm::StringRef sym_name, ::mlir::SymbolRefAttr target, ::mlir::FunctionType function_type, ::mlir::ArrayAttr arg_attrs, ::mlir::ArrayAttr res_attrs) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(sym_name)>(sym_name), std::forward<decltype(target)>(target), std::forward<decltype(function_type)>(function_type), std::forward<decltype(arg_attrs)>(arg_attrs), std::forward<decltype(res_attrs)>(res_attrs));
  auto __res__ = ::llvm::dyn_cast<ContractOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
ContractOp ContractOp::create(::mlir::ImplicitLocOpBuilder &builder, ::llvm::StringRef sym_name, ::mlir::SymbolRefAttr target, ::mlir::FunctionType function_type, ::mlir::ArrayAttr arg_attrs, ::mlir::ArrayAttr res_attrs) {
  return create(builder, builder.getLoc(), std::forward<decltype(sym_name)>(sym_name), std::forward<decltype(target)>(target), std::forward<decltype(function_type)>(function_type), std::forward<decltype(arg_attrs)>(arg_attrs), std::forward<decltype(res_attrs)>(res_attrs));
}
 
void ContractOp::build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, ::mlir::TypeRange resultTypes, ::llvm::StringRef sym_name, ::mlir::SymbolRefAttr target, ::mlir::FunctionType function_type, ::mlir::ArrayAttr arg_attrs, ::mlir::ArrayAttr res_attrs) {
        odsState.getOrAddProperties<Properties>().sym_name = odsBuilder.getStringAttr(sym_name);
        odsState.getOrAddProperties<Properties>().target = target;
        odsState.getOrAddProperties<Properties>().function_type = ::mlir::TypeAttr::get(function_type);
        if (arg_attrs) {
          odsState.getOrAddProperties<Properties>().arg_attrs = arg_attrs;
        }
        if (res_attrs) {
          odsState.getOrAddProperties<Properties>().res_attrs = res_attrs;
        }
        initializeEmptyBody(odsBuilder, odsState, function_type);
        assert(resultTypes.size() == 0u && "mismatched number of results");
        odsState.addTypes(resultTypes);
      
}
 
ContractOp ContractOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::TypeRange resultTypes, ::llvm::StringRef sym_name, ::mlir::SymbolRefAttr target, ::mlir::FunctionType function_type, ::mlir::ArrayAttr arg_attrs, ::mlir::ArrayAttr res_attrs) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(sym_name)>(sym_name), std::forward<decltype(target)>(target), std::forward<decltype(function_type)>(function_type), std::forward<decltype(arg_attrs)>(arg_attrs), std::forward<decltype(res_attrs)>(res_attrs));
  auto __res__ = ::llvm::dyn_cast<ContractOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
ContractOp ContractOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::TypeRange resultTypes, ::llvm::StringRef sym_name, ::mlir::SymbolRefAttr target, ::mlir::FunctionType function_type, ::mlir::ArrayAttr arg_attrs, ::mlir::ArrayAttr res_attrs) {
  return create(builder, builder.getLoc(), std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(sym_name)>(sym_name), std::forward<decltype(target)>(target), std::forward<decltype(function_type)>(function_type), std::forward<decltype(arg_attrs)>(arg_attrs), std::forward<decltype(res_attrs)>(res_attrs));
}
 
ContractOp ContractOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::llvm::StringRef name, llvm::StringRef target) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(name)>(name), std::forward<decltype(target)>(target));
  auto __res__ = ::llvm::dyn_cast<ContractOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
ContractOp ContractOp::create(::mlir::ImplicitLocOpBuilder &builder, ::llvm::StringRef name, llvm::StringRef target) {
  return create(builder, builder.getLoc(), std::forward<decltype(name)>(name), std::forward<decltype(target)>(target));
}
 
ContractOp ContractOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::llvm::StringRef name, ::mlir::SymbolRefAttr target) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(name)>(name), std::forward<decltype(target)>(target));
  auto __res__ = ::llvm::dyn_cast<ContractOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
ContractOp ContractOp::create(::mlir::ImplicitLocOpBuilder &builder, ::llvm::StringRef name, ::mlir::SymbolRefAttr target) {
  return create(builder, builder.getLoc(), std::forward<decltype(name)>(name), std::forward<decltype(target)>(target));
}
 
::llvm::LogicalResult ContractOp::verifyInvariantsImpl() {
  auto tblgen_arg_attrs = getProperties().arg_attrs; (void)tblgen_arg_attrs;
  auto tblgen_function_type = getProperties().function_type; (void)tblgen_function_type;
  if (!tblgen_function_type) return emitOpError("requires attribute 'function_type'");
  auto tblgen_res_attrs = getProperties().res_attrs; (void)tblgen_res_attrs;
  auto tblgen_sym_name = getProperties().sym_name; (void)tblgen_sym_name;
  if (!tblgen_sym_name) return emitOpError("requires attribute 'sym_name'");
  auto tblgen_target = getProperties().target; (void)tblgen_target;
  if (!tblgen_target) return emitOpError("requires attribute 'target'");
 
  if (::mlir::failed(__mlir_ods_local_attr_constraint_Ops1(*this, tblgen_sym_name, "sym_name")))
    return ::mlir::failure();
 
  if (::mlir::failed(__mlir_ods_local_attr_constraint_Ops2(*this, tblgen_target, "target")))
    return ::mlir::failure();
 
  if (::mlir::failed(__mlir_ods_local_attr_constraint_Ops3(*this, tblgen_function_type, "function_type")))
    return ::mlir::failure();
 
  if (::mlir::failed(__mlir_ods_local_attr_constraint_Ops4(*this, tblgen_arg_attrs, "arg_attrs")))
    return ::mlir::failure();
 
  if (::mlir::failed(__mlir_ods_local_attr_constraint_Ops4(*this, tblgen_res_attrs, "res_attrs")))
    return ::mlir::failure();
  {
    unsigned index = 0; (void)index;
 
    for (auto &region : ::llvm::MutableArrayRef((*this)->getRegion(0)))
      if (::mlir::failed(__mlir_ods_local_region_constraint_Ops1(*this, region, "body", index++)))
        return ::mlir::failure();
  }
  return ::mlir::success();
}
 
::llvm::LogicalResult ContractOp::verifyInvariants() {
  if(::mlir::succeeded(verifyInvariantsImpl()) && ::mlir::succeeded(verify()))
    return ::mlir::success();
  return ::mlir::failure();
}
 
::llvm::LogicalResult ContractOp::setPropertiesFromParsedAttr(Properties &prop, ::mlir::Attribute attr, ::llvm::function_ref<::mlir::InFlightDiagnostic()> emitError) {
  ::mlir::DictionaryAttr dict = ::llvm::dyn_cast<::mlir::DictionaryAttr>(attr);
  if (!dict) {
    emitError() << "expected DictionaryAttr to set properties";
    return ::mlir::failure();
  }
  // keep track of used keys in the input dictionary to be able to error out
  // if there are some unknown ones.
  ::mlir::DenseSet<::mlir::StringAttr> usedKeys;
  ::mlir::MLIRContext *ctx = dict.getContext();
  (void)ctx;
  {
 
    auto &propStorage = prop.sym_name;
    auto sym_nameAttrName = ::mlir::StringAttr::get(ctx, "sym_name");
    auto attr = dict.get(sym_nameAttrName);
    usedKeys.insert(sym_nameAttrName);
    if (attr || /*isRequired=*/true) {
      if (!attr) {
        emitError() << "expected key entry for sym_name in DictionaryAttr to set "
                   "Properties.";
        return ::mlir::failure();
      }
      auto convertedAttr = ::llvm::dyn_cast<std::remove_reference_t<decltype(propStorage)>>(attr);
      if (convertedAttr) {
        propStorage = convertedAttr;
      } else {
        emitError() << "Invalid attribute `sym_name` in property conversion: " << attr;
        return ::mlir::failure();
      }
    }
  }
  {
 
    auto &propStorage = prop.target;
    auto targetAttrName = ::mlir::StringAttr::get(ctx, "target");
    auto attr = dict.get(targetAttrName);
    usedKeys.insert(targetAttrName);
    if (attr || /*isRequired=*/true) {
      if (!attr) {
        emitError() << "expected key entry for target in DictionaryAttr to set "
                   "Properties.";
        return ::mlir::failure();
      }
      auto convertedAttr = ::llvm::dyn_cast<std::remove_reference_t<decltype(propStorage)>>(attr);
      if (convertedAttr) {
        propStorage = convertedAttr;
      } else {
        emitError() << "Invalid attribute `target` in property conversion: " << attr;
        return ::mlir::failure();
      }
    }
  }
  {
 
    auto &propStorage = prop.function_type;
    auto function_typeAttrName = ::mlir::StringAttr::get(ctx, "function_type");
    auto attr = dict.get(function_typeAttrName);
    usedKeys.insert(function_typeAttrName);
    if (attr || /*isRequired=*/true) {
      if (!attr) {
        emitError() << "expected key entry for function_type in DictionaryAttr to set "
                   "Properties.";
        return ::mlir::failure();
      }
      auto convertedAttr = ::llvm::dyn_cast<std::remove_reference_t<decltype(propStorage)>>(attr);
      if (convertedAttr) {
        propStorage = convertedAttr;
      } else {
        emitError() << "Invalid attribute `function_type` in property conversion: " << attr;
        return ::mlir::failure();
      }
    }
  }
  {
 
    auto &propStorage = prop.arg_attrs;
    auto arg_attrsAttrName = ::mlir::StringAttr::get(ctx, "arg_attrs");
    auto attr = dict.get(arg_attrsAttrName);
    usedKeys.insert(arg_attrsAttrName);
    if (attr || /*isRequired=*/false) {
      if (!attr) {
        emitError() << "expected key entry for arg_attrs in DictionaryAttr to set "
                   "Properties.";
        return ::mlir::failure();
      }
      auto convertedAttr = ::llvm::dyn_cast<std::remove_reference_t<decltype(propStorage)>>(attr);
      if (convertedAttr) {
        propStorage = convertedAttr;
      } else {
        emitError() << "Invalid attribute `arg_attrs` in property conversion: " << attr;
        return ::mlir::failure();
      }
    }
  }
  {
 
    auto &propStorage = prop.res_attrs;
    auto res_attrsAttrName = ::mlir::StringAttr::get(ctx, "res_attrs");
    auto attr = dict.get(res_attrsAttrName);
    usedKeys.insert(res_attrsAttrName);
    if (attr || /*isRequired=*/false) {
      if (!attr) {
        emitError() << "expected key entry for res_attrs in DictionaryAttr to set "
                   "Properties.";
        return ::mlir::failure();
      }
      auto convertedAttr = ::llvm::dyn_cast<std::remove_reference_t<decltype(propStorage)>>(attr);
      if (convertedAttr) {
        propStorage = convertedAttr;
      } else {
        emitError() << "Invalid attribute `res_attrs` in property conversion: " << attr;
        return ::mlir::failure();
      }
    }
  }
 
  for (::mlir::NamedAttribute attr : dict) {
    if (!usedKeys.contains(attr.getName()))
      return emitError() << "unknown key '" << attr.getName() <<
          "' when parsing properties dictionary";
  }
  return ::mlir::success();
}
 
 
} // namespace llzk::verif
MLIR_DEFINE_EXPLICIT_TYPE_ID(::llzk::verif::ContractOp)
MLIR_DEFINE_EXPLICIT_TYPE_ID(::llzk::verif::detail::ContractOpGenericAdaptorBase::Properties)
 
namespace llzk::verif {
 
 
//===----------------------------------------------------------------------===//
// ::llzk::verif::DecreasesOp definitions
//===----------------------------------------------------------------------===//
 
namespace detail {
 
DecreasesOpGenericAdaptorBase::DecreasesOpGenericAdaptorBase(DecreasesOp op) : odsAttrs(op->getRawDictionaryAttrs()), odsOpName(op->getName()), properties(op.getProperties()), odsRegions(op->getRegions()) {}
 
 
} // namespace detail
DecreasesOpAdaptor::DecreasesOpAdaptor(DecreasesOp op) : DecreasesOpGenericAdaptor(op->getOperands(), op) {}
 
::llvm::LogicalResult DecreasesOpAdaptor::verify(::mlir::Location loc) {
  return ::mlir::success();
}
 
::llvm::LogicalResult DecreasesOp::setPropertiesFromAttr(Properties &prop, ::mlir::Attribute attr, ::llvm::function_ref<::mlir::InFlightDiagnostic()> emitError) {
  ::mlir::DictionaryAttr dict = ::llvm::dyn_cast<::mlir::DictionaryAttr>(attr);
  if (!dict) {
    emitError() << "expected DictionaryAttr to set properties";
    return ::mlir::failure();
  }
      return ::mlir::success();
}
 
::mlir::Attribute DecreasesOp::getPropertiesAsAttr(::mlir::MLIRContext *ctx, const Properties &prop) {
    ::mlir::SmallVector<::mlir::NamedAttribute> attrs;
    ::mlir::Builder odsBuilder{ctx};
 
  if (!attrs.empty())
    return odsBuilder.getDictionaryAttr(attrs);
  return {};
}
 
llvm::hash_code DecreasesOp::computePropertiesHash(const Properties &prop) {
  using llvm::hash_value;
  return llvm::hash_combine();
}
 
std::optional<mlir::Attribute> DecreasesOp::getInherentAttr(::mlir::MLIRContext *ctx, const Properties &prop, llvm::StringRef name) {
  return std::nullopt;
}
 
void DecreasesOp::setInherentAttr(Properties &prop, llvm::StringRef name, mlir::Attribute value) {
}
 
void DecreasesOp::populateInherentAttrs(::mlir::MLIRContext *ctx, const Properties &prop, ::mlir::NamedAttrList &attrs) {
}
 
::llvm::LogicalResult DecreasesOp::verifyInherentAttrs(::mlir::OperationName opName, ::mlir::NamedAttrList &attrs, llvm::function_ref<::mlir::InFlightDiagnostic()> emitError) {
    return ::mlir::success();
}
 
void DecreasesOp::build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, ::mlir::Value value) {
  odsState.addOperands(value);
}
 
DecreasesOp DecreasesOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::Value value) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(value)>(value));
  auto __res__ = ::llvm::dyn_cast<DecreasesOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
DecreasesOp DecreasesOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::Value value) {
  return create(builder, builder.getLoc(), std::forward<decltype(value)>(value));
}
 
void DecreasesOp::build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, ::mlir::TypeRange resultTypes, ::mlir::Value value) {
  odsState.addOperands(value);
  assert(resultTypes.size() == 0u && "mismatched number of results");
  odsState.addTypes(resultTypes);
}
 
DecreasesOp DecreasesOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::TypeRange resultTypes, ::mlir::Value value) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(value)>(value));
  auto __res__ = ::llvm::dyn_cast<DecreasesOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
DecreasesOp DecreasesOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::TypeRange resultTypes, ::mlir::Value value) {
  return create(builder, builder.getLoc(), std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(value)>(value));
}
 
void DecreasesOp::build(::mlir::OpBuilder &, ::mlir::OperationState &odsState, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, ::llvm::ArrayRef<::mlir::NamedAttribute> attributes) {
  assert(operands.size() == 1u && "mismatched number of parameters");
  odsState.addOperands(operands);
  odsState.addAttributes(attributes);
  assert(resultTypes.size() == 0u && "mismatched number of return types");
  odsState.addTypes(resultTypes);
}
 
DecreasesOp DecreasesOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, ::llvm::ArrayRef<::mlir::NamedAttribute> attributes) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(operands)>(operands), std::forward<decltype(attributes)>(attributes));
  auto __res__ = ::llvm::dyn_cast<DecreasesOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
DecreasesOp DecreasesOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, ::llvm::ArrayRef<::mlir::NamedAttribute> attributes) {
  return create(builder, builder.getLoc(), std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(operands)>(operands), std::forward<decltype(attributes)>(attributes));
}
 
void DecreasesOp::build(::mlir::OpBuilder &, ::mlir::OperationState &odsState, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, const Properties &properties, ::llvm::ArrayRef<::mlir::NamedAttribute> discardableAttributes) {
  assert(operands.size() == 1u && "mismatched number of parameters");
  odsState.addOperands(operands);
  odsState.useProperties(const_cast<Properties&>(properties));
  odsState.addAttributes(discardableAttributes);
  assert(resultTypes.size() == 0u && "mismatched number of return types");
  odsState.addTypes(resultTypes);
}
 
DecreasesOp DecreasesOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, const Properties &properties, ::llvm::ArrayRef<::mlir::NamedAttribute> discardableAttributes) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(operands)>(operands), std::forward<decltype(properties)>(properties), std::forward<decltype(discardableAttributes)>(discardableAttributes));
  auto __res__ = ::llvm::dyn_cast<DecreasesOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
DecreasesOp DecreasesOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, const Properties &properties, ::llvm::ArrayRef<::mlir::NamedAttribute> discardableAttributes) {
  return create(builder, builder.getLoc(), std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(operands)>(operands), std::forward<decltype(properties)>(properties), std::forward<decltype(discardableAttributes)>(discardableAttributes));
}
 
::llvm::LogicalResult DecreasesOp::verifyInvariantsImpl() {
  {
    unsigned index = 0; (void)index;
    auto valueGroup0 = getODSOperands(0);
 
    for (auto v : valueGroup0) {
      if (::mlir::failed(__mlir_ods_local_type_constraint_Ops2(*this, v.getType(), "operand", index++)))
        return ::mlir::failure();
    }
  }
  return ::mlir::success();
}
 
::llvm::LogicalResult DecreasesOp::verifyInvariants() {
  return verifyInvariantsImpl();
}
 
::mlir::ParseResult DecreasesOp::parse(::mlir::OpAsmParser &parser, ::mlir::OperationState &result) {
  ::mlir::OpAsmParser::UnresolvedOperand valueRawOperand{};
  ::llvm::ArrayRef<::mlir::OpAsmParser::UnresolvedOperand> valueOperands(&valueRawOperand, 1);  ::llvm::SMLoc valueOperandsLoc;
  (void)valueOperandsLoc;
 
  valueOperandsLoc = parser.getCurrentLocation();
  if (parser.parseOperand(valueRawOperand))
    return ::mlir::failure();
  {
    auto loc = parser.getCurrentLocation();(void)loc;
    if (parser.parseOptionalAttrDict(result.attributes))
      return ::mlir::failure();
    if (failed(verifyInherentAttrs(result.name, result.attributes, [&]() {
        return parser.emitError(loc) << "'" << result.name.getStringRef() << "' op ";
      })))
      return ::mlir::failure();
  }
  ::mlir::Type odsBuildableType0 = ::llzk::felt::FeltType::get(parser.getBuilder().getContext());
  if (parser.resolveOperands(valueOperands, odsBuildableType0, valueOperandsLoc, result.operands))
    return ::mlir::failure();
  return ::mlir::success();
}
 
void DecreasesOp::print(::mlir::OpAsmPrinter &_odsPrinter) {
  _odsPrinter << ' ';
  _odsPrinter << getValue();
  ::llvm::SmallVector<::llvm::StringRef, 2> elidedAttrs;
  _odsPrinter.printOptionalAttrDict((*this)->getAttrs(), elidedAttrs);
}
 
// This side effect models "program termination". Based on
// https://github.com/llvm/llvm-project/blob/f325e4b2d836d6e65a4d0cf3efc6b0996ccf3765/mlir/lib/Dialect/ControlFlow/IR/ControlFlowOps.cpp#L92-L97
void DecreasesOp::getEffects(
    ::mlir::SmallVectorImpl<::mlir::SideEffects::EffectInstance<::mlir::MemoryEffects::Effect>> &effects
) {
  effects.emplace_back(::mlir::MemoryEffects::Write::get());
}
 
} // namespace llzk::verif
MLIR_DEFINE_EXPLICIT_TYPE_ID(::llzk::verif::DecreasesOp)
 
namespace llzk::verif {
 
 
//===----------------------------------------------------------------------===//
// ::llzk::verif::EnsureComputeOp definitions
//===----------------------------------------------------------------------===//
 
namespace detail {
 
EnsureComputeOpGenericAdaptorBase::EnsureComputeOpGenericAdaptorBase(EnsureComputeOp op) : odsAttrs(op->getRawDictionaryAttrs()), odsOpName(op->getName()), properties(op.getProperties()), odsRegions(op->getRegions()) {}
 
 
} // namespace detail
EnsureComputeOpAdaptor::EnsureComputeOpAdaptor(EnsureComputeOp op) : EnsureComputeOpGenericAdaptor(op->getOperands(), op) {}
 
::llvm::LogicalResult EnsureComputeOpAdaptor::verify(::mlir::Location loc) {
  return ::mlir::success();
}
 
::llvm::LogicalResult EnsureComputeOp::setPropertiesFromAttr(Properties &prop, ::mlir::Attribute attr, ::llvm::function_ref<::mlir::InFlightDiagnostic()> emitError) {
  ::mlir::DictionaryAttr dict = ::llvm::dyn_cast<::mlir::DictionaryAttr>(attr);
  if (!dict) {
    emitError() << "expected DictionaryAttr to set properties";
    return ::mlir::failure();
  }
      return ::mlir::success();
}
 
::mlir::Attribute EnsureComputeOp::getPropertiesAsAttr(::mlir::MLIRContext *ctx, const Properties &prop) {
    ::mlir::SmallVector<::mlir::NamedAttribute> attrs;
    ::mlir::Builder odsBuilder{ctx};
 
  if (!attrs.empty())
    return odsBuilder.getDictionaryAttr(attrs);
  return {};
}
 
llvm::hash_code EnsureComputeOp::computePropertiesHash(const Properties &prop) {
  using llvm::hash_value;
  return llvm::hash_combine();
}
 
std::optional<mlir::Attribute> EnsureComputeOp::getInherentAttr(::mlir::MLIRContext *ctx, const Properties &prop, llvm::StringRef name) {
  return std::nullopt;
}
 
void EnsureComputeOp::setInherentAttr(Properties &prop, llvm::StringRef name, mlir::Attribute value) {
}
 
void EnsureComputeOp::populateInherentAttrs(::mlir::MLIRContext *ctx, const Properties &prop, ::mlir::NamedAttrList &attrs) {
}
 
::llvm::LogicalResult EnsureComputeOp::verifyInherentAttrs(::mlir::OperationName opName, ::mlir::NamedAttrList &attrs, llvm::function_ref<::mlir::InFlightDiagnostic()> emitError) {
    return ::mlir::success();
}
 
void EnsureComputeOp::build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, ::mlir::Value condition) {
  odsState.addOperands(condition);
}
 
EnsureComputeOp EnsureComputeOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::Value condition) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(condition)>(condition));
  auto __res__ = ::llvm::dyn_cast<EnsureComputeOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
EnsureComputeOp EnsureComputeOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::Value condition) {
  return create(builder, builder.getLoc(), std::forward<decltype(condition)>(condition));
}
 
void EnsureComputeOp::build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, ::mlir::TypeRange resultTypes, ::mlir::Value condition) {
  odsState.addOperands(condition);
  assert(resultTypes.size() == 0u && "mismatched number of results");
  odsState.addTypes(resultTypes);
}
 
EnsureComputeOp EnsureComputeOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::TypeRange resultTypes, ::mlir::Value condition) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(condition)>(condition));
  auto __res__ = ::llvm::dyn_cast<EnsureComputeOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
EnsureComputeOp EnsureComputeOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::TypeRange resultTypes, ::mlir::Value condition) {
  return create(builder, builder.getLoc(), std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(condition)>(condition));
}
 
void EnsureComputeOp::build(::mlir::OpBuilder &, ::mlir::OperationState &odsState, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, ::llvm::ArrayRef<::mlir::NamedAttribute> attributes) {
  assert(operands.size() == 1u && "mismatched number of parameters");
  odsState.addOperands(operands);
  odsState.addAttributes(attributes);
  assert(resultTypes.size() == 0u && "mismatched number of return types");
  odsState.addTypes(resultTypes);
}
 
EnsureComputeOp EnsureComputeOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, ::llvm::ArrayRef<::mlir::NamedAttribute> attributes) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(operands)>(operands), std::forward<decltype(attributes)>(attributes));
  auto __res__ = ::llvm::dyn_cast<EnsureComputeOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
EnsureComputeOp EnsureComputeOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, ::llvm::ArrayRef<::mlir::NamedAttribute> attributes) {
  return create(builder, builder.getLoc(), std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(operands)>(operands), std::forward<decltype(attributes)>(attributes));
}
 
void EnsureComputeOp::build(::mlir::OpBuilder &, ::mlir::OperationState &odsState, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, const Properties &properties, ::llvm::ArrayRef<::mlir::NamedAttribute> discardableAttributes) {
  assert(operands.size() == 1u && "mismatched number of parameters");
  odsState.addOperands(operands);
  odsState.useProperties(const_cast<Properties&>(properties));
  odsState.addAttributes(discardableAttributes);
  assert(resultTypes.size() == 0u && "mismatched number of return types");
  odsState.addTypes(resultTypes);
}
 
EnsureComputeOp EnsureComputeOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, const Properties &properties, ::llvm::ArrayRef<::mlir::NamedAttribute> discardableAttributes) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(operands)>(operands), std::forward<decltype(properties)>(properties), std::forward<decltype(discardableAttributes)>(discardableAttributes));
  auto __res__ = ::llvm::dyn_cast<EnsureComputeOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
EnsureComputeOp EnsureComputeOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, const Properties &properties, ::llvm::ArrayRef<::mlir::NamedAttribute> discardableAttributes) {
  return create(builder, builder.getLoc(), std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(operands)>(operands), std::forward<decltype(properties)>(properties), std::forward<decltype(discardableAttributes)>(discardableAttributes));
}
 
::llvm::LogicalResult EnsureComputeOp::verifyInvariantsImpl() {
  {
    unsigned index = 0; (void)index;
    auto valueGroup0 = getODSOperands(0);
 
    for (auto v : valueGroup0) {
      if (::mlir::failed(__mlir_ods_local_type_constraint_Ops3(*this, v.getType(), "operand", index++)))
        return ::mlir::failure();
    }
  }
  return ::mlir::success();
}
 
::llvm::LogicalResult EnsureComputeOp::verifyInvariants() {
  return verifyInvariantsImpl();
}
 
::mlir::ParseResult EnsureComputeOp::parse(::mlir::OpAsmParser &parser, ::mlir::OperationState &result) {
  ::mlir::OpAsmParser::UnresolvedOperand conditionRawOperand{};
  ::llvm::ArrayRef<::mlir::OpAsmParser::UnresolvedOperand> conditionOperands(&conditionRawOperand, 1);  ::llvm::SMLoc conditionOperandsLoc;
  (void)conditionOperandsLoc;
 
  conditionOperandsLoc = parser.getCurrentLocation();
  if (parser.parseOperand(conditionRawOperand))
    return ::mlir::failure();
  {
    auto loc = parser.getCurrentLocation();(void)loc;
    if (parser.parseOptionalAttrDict(result.attributes))
      return ::mlir::failure();
    if (failed(verifyInherentAttrs(result.name, result.attributes, [&]() {
        return parser.emitError(loc) << "'" << result.name.getStringRef() << "' op ";
      })))
      return ::mlir::failure();
  }
  ::mlir::Type odsBuildableType0 = parser.getBuilder().getIntegerType(1);
  if (parser.resolveOperands(conditionOperands, odsBuildableType0, conditionOperandsLoc, result.operands))
    return ::mlir::failure();
  return ::mlir::success();
}
 
void EnsureComputeOp::print(::mlir::OpAsmPrinter &_odsPrinter) {
  _odsPrinter << ' ';
  _odsPrinter << getCondition();
  ::llvm::SmallVector<::llvm::StringRef, 2> elidedAttrs;
  _odsPrinter.printOptionalAttrDict((*this)->getAttrs(), elidedAttrs);
}
 
// This side effect models "program termination". Based on
// https://github.com/llvm/llvm-project/blob/f325e4b2d836d6e65a4d0cf3efc6b0996ccf3765/mlir/lib/Dialect/ControlFlow/IR/ControlFlowOps.cpp#L92-L97
void EnsureComputeOp::getEffects(
    ::mlir::SmallVectorImpl<::mlir::SideEffects::EffectInstance<::mlir::MemoryEffects::Effect>> &effects
) {
  effects.emplace_back(::mlir::MemoryEffects::Write::get());
}
 
} // namespace llzk::verif
MLIR_DEFINE_EXPLICIT_TYPE_ID(::llzk::verif::EnsureComputeOp)
 
namespace llzk::verif {
 
 
//===----------------------------------------------------------------------===//
// ::llzk::verif::EnsureConstrainOp definitions
//===----------------------------------------------------------------------===//
 
namespace detail {
 
EnsureConstrainOpGenericAdaptorBase::EnsureConstrainOpGenericAdaptorBase(EnsureConstrainOp op) : odsAttrs(op->getRawDictionaryAttrs()), odsOpName(op->getName()), properties(op.getProperties()), odsRegions(op->getRegions()) {}
 
 
} // namespace detail
EnsureConstrainOpAdaptor::EnsureConstrainOpAdaptor(EnsureConstrainOp op) : EnsureConstrainOpGenericAdaptor(op->getOperands(), op) {}
 
::llvm::LogicalResult EnsureConstrainOpAdaptor::verify(::mlir::Location loc) {
  return ::mlir::success();
}
 
::llvm::LogicalResult EnsureConstrainOp::setPropertiesFromAttr(Properties &prop, ::mlir::Attribute attr, ::llvm::function_ref<::mlir::InFlightDiagnostic()> emitError) {
  ::mlir::DictionaryAttr dict = ::llvm::dyn_cast<::mlir::DictionaryAttr>(attr);
  if (!dict) {
    emitError() << "expected DictionaryAttr to set properties";
    return ::mlir::failure();
  }
      return ::mlir::success();
}
 
::mlir::Attribute EnsureConstrainOp::getPropertiesAsAttr(::mlir::MLIRContext *ctx, const Properties &prop) {
    ::mlir::SmallVector<::mlir::NamedAttribute> attrs;
    ::mlir::Builder odsBuilder{ctx};
 
  if (!attrs.empty())
    return odsBuilder.getDictionaryAttr(attrs);
  return {};
}
 
llvm::hash_code EnsureConstrainOp::computePropertiesHash(const Properties &prop) {
  using llvm::hash_value;
  return llvm::hash_combine();
}
 
std::optional<mlir::Attribute> EnsureConstrainOp::getInherentAttr(::mlir::MLIRContext *ctx, const Properties &prop, llvm::StringRef name) {
  return std::nullopt;
}
 
void EnsureConstrainOp::setInherentAttr(Properties &prop, llvm::StringRef name, mlir::Attribute value) {
}
 
void EnsureConstrainOp::populateInherentAttrs(::mlir::MLIRContext *ctx, const Properties &prop, ::mlir::NamedAttrList &attrs) {
}
 
::llvm::LogicalResult EnsureConstrainOp::verifyInherentAttrs(::mlir::OperationName opName, ::mlir::NamedAttrList &attrs, llvm::function_ref<::mlir::InFlightDiagnostic()> emitError) {
    return ::mlir::success();
}
 
void EnsureConstrainOp::build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, ::mlir::Value condition) {
  odsState.addOperands(condition);
}
 
EnsureConstrainOp EnsureConstrainOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::Value condition) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(condition)>(condition));
  auto __res__ = ::llvm::dyn_cast<EnsureConstrainOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
EnsureConstrainOp EnsureConstrainOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::Value condition) {
  return create(builder, builder.getLoc(), std::forward<decltype(condition)>(condition));
}
 
void EnsureConstrainOp::build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, ::mlir::TypeRange resultTypes, ::mlir::Value condition) {
  odsState.addOperands(condition);
  assert(resultTypes.size() == 0u && "mismatched number of results");
  odsState.addTypes(resultTypes);
}
 
EnsureConstrainOp EnsureConstrainOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::TypeRange resultTypes, ::mlir::Value condition) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(condition)>(condition));
  auto __res__ = ::llvm::dyn_cast<EnsureConstrainOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
EnsureConstrainOp EnsureConstrainOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::TypeRange resultTypes, ::mlir::Value condition) {
  return create(builder, builder.getLoc(), std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(condition)>(condition));
}
 
void EnsureConstrainOp::build(::mlir::OpBuilder &, ::mlir::OperationState &odsState, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, ::llvm::ArrayRef<::mlir::NamedAttribute> attributes) {
  assert(operands.size() == 1u && "mismatched number of parameters");
  odsState.addOperands(operands);
  odsState.addAttributes(attributes);
  assert(resultTypes.size() == 0u && "mismatched number of return types");
  odsState.addTypes(resultTypes);
}
 
EnsureConstrainOp EnsureConstrainOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, ::llvm::ArrayRef<::mlir::NamedAttribute> attributes) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(operands)>(operands), std::forward<decltype(attributes)>(attributes));
  auto __res__ = ::llvm::dyn_cast<EnsureConstrainOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
EnsureConstrainOp EnsureConstrainOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, ::llvm::ArrayRef<::mlir::NamedAttribute> attributes) {
  return create(builder, builder.getLoc(), std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(operands)>(operands), std::forward<decltype(attributes)>(attributes));
}
 
void EnsureConstrainOp::build(::mlir::OpBuilder &, ::mlir::OperationState &odsState, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, const Properties &properties, ::llvm::ArrayRef<::mlir::NamedAttribute> discardableAttributes) {
  assert(operands.size() == 1u && "mismatched number of parameters");
  odsState.addOperands(operands);
  odsState.useProperties(const_cast<Properties&>(properties));
  odsState.addAttributes(discardableAttributes);
  assert(resultTypes.size() == 0u && "mismatched number of return types");
  odsState.addTypes(resultTypes);
}
 
EnsureConstrainOp EnsureConstrainOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, const Properties &properties, ::llvm::ArrayRef<::mlir::NamedAttribute> discardableAttributes) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(operands)>(operands), std::forward<decltype(properties)>(properties), std::forward<decltype(discardableAttributes)>(discardableAttributes));
  auto __res__ = ::llvm::dyn_cast<EnsureConstrainOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
EnsureConstrainOp EnsureConstrainOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, const Properties &properties, ::llvm::ArrayRef<::mlir::NamedAttribute> discardableAttributes) {
  return create(builder, builder.getLoc(), std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(operands)>(operands), std::forward<decltype(properties)>(properties), std::forward<decltype(discardableAttributes)>(discardableAttributes));
}
 
::llvm::LogicalResult EnsureConstrainOp::verifyInvariantsImpl() {
  {
    unsigned index = 0; (void)index;
    auto valueGroup0 = getODSOperands(0);
 
    for (auto v : valueGroup0) {
      if (::mlir::failed(__mlir_ods_local_type_constraint_Ops3(*this, v.getType(), "operand", index++)))
        return ::mlir::failure();
    }
  }
  return ::mlir::success();
}
 
::llvm::LogicalResult EnsureConstrainOp::verifyInvariants() {
  return verifyInvariantsImpl();
}
 
::mlir::ParseResult EnsureConstrainOp::parse(::mlir::OpAsmParser &parser, ::mlir::OperationState &result) {
  ::mlir::OpAsmParser::UnresolvedOperand conditionRawOperand{};
  ::llvm::ArrayRef<::mlir::OpAsmParser::UnresolvedOperand> conditionOperands(&conditionRawOperand, 1);  ::llvm::SMLoc conditionOperandsLoc;
  (void)conditionOperandsLoc;
 
  conditionOperandsLoc = parser.getCurrentLocation();
  if (parser.parseOperand(conditionRawOperand))
    return ::mlir::failure();
  {
    auto loc = parser.getCurrentLocation();(void)loc;
    if (parser.parseOptionalAttrDict(result.attributes))
      return ::mlir::failure();
    if (failed(verifyInherentAttrs(result.name, result.attributes, [&]() {
        return parser.emitError(loc) << "'" << result.name.getStringRef() << "' op ";
      })))
      return ::mlir::failure();
  }
  ::mlir::Type odsBuildableType0 = parser.getBuilder().getIntegerType(1);
  if (parser.resolveOperands(conditionOperands, odsBuildableType0, conditionOperandsLoc, result.operands))
    return ::mlir::failure();
  return ::mlir::success();
}
 
void EnsureConstrainOp::print(::mlir::OpAsmPrinter &_odsPrinter) {
  _odsPrinter << ' ';
  _odsPrinter << getCondition();
  ::llvm::SmallVector<::llvm::StringRef, 2> elidedAttrs;
  _odsPrinter.printOptionalAttrDict((*this)->getAttrs(), elidedAttrs);
}
 
// This side effect models "program termination". Based on
// https://github.com/llvm/llvm-project/blob/f325e4b2d836d6e65a4d0cf3efc6b0996ccf3765/mlir/lib/Dialect/ControlFlow/IR/ControlFlowOps.cpp#L92-L97
void EnsureConstrainOp::getEffects(
    ::mlir::SmallVectorImpl<::mlir::SideEffects::EffectInstance<::mlir::MemoryEffects::Effect>> &effects
) {
  effects.emplace_back(::mlir::MemoryEffects::Write::get());
}
 
} // namespace llzk::verif
MLIR_DEFINE_EXPLICIT_TYPE_ID(::llzk::verif::EnsureConstrainOp)
 
namespace llzk::verif {
 
 
//===----------------------------------------------------------------------===//
// ::llzk::verif::IncludeOp definitions
//===----------------------------------------------------------------------===//
 
namespace detail {
 
IncludeOpGenericAdaptorBase::IncludeOpGenericAdaptorBase(IncludeOp op) : odsAttrs(op->getRawDictionaryAttrs()), odsOpName(op->getName()), properties(op.getProperties()), odsRegions(op->getRegions()) {}
 
std::pair<unsigned, unsigned> IncludeOpGenericAdaptorBase::getODSOperandIndexAndLength(unsigned index, unsigned odsOperandsSize) {
  ::llvm::ArrayRef<int32_t> sizeAttr = getProperties().operandSegmentSizes;
 
  unsigned start = 0;
  for (unsigned i = 0; i < index; ++i)
    start += sizeAttr[i];
  return {start, sizeAttr[index]};
}
 
::mlir::SymbolRefAttr IncludeOpGenericAdaptorBase::getCallee() {
  auto attr = getCalleeAttr();
  return attr;
}
 
::std::optional< ::mlir::ArrayAttr > IncludeOpGenericAdaptorBase::getTemplateParams() {
  auto attr = getTemplateParamsAttr();
  return attr ? ::std::optional< ::mlir::ArrayAttr >(attr) : (::std::nullopt);
}
 
::mlir::DenseI32ArrayAttr IncludeOpGenericAdaptorBase::getNumDimsPerMapAttr() {
  auto attr = ::llvm::dyn_cast_or_null<::mlir::DenseI32ArrayAttr>(getProperties().numDimsPerMap);
  return attr;
}
 
::llvm::ArrayRef<int32_t> IncludeOpGenericAdaptorBase::getNumDimsPerMap() {
  auto attr = getNumDimsPerMapAttr();
  return attr;
}
 
::llvm::ArrayRef<int32_t> IncludeOpGenericAdaptorBase::getMapOpGroupSizes() {
  auto attr = getMapOpGroupSizesAttr();
  return attr;
}
 
::std::optional< ::mlir::ArrayAttr > IncludeOpGenericAdaptorBase::getArgAttrs() {
  auto attr = getArgAttrsAttr();
  return attr ? ::std::optional< ::mlir::ArrayAttr >(attr) : (::std::nullopt);
}
 
::std::optional< ::mlir::ArrayAttr > IncludeOpGenericAdaptorBase::getResAttrs() {
  auto attr = getResAttrsAttr();
  return attr ? ::std::optional< ::mlir::ArrayAttr >(attr) : (::std::nullopt);
}
 
 
} // namespace detail
IncludeOpAdaptor::IncludeOpAdaptor(IncludeOp op) : IncludeOpGenericAdaptor(op->getOperands(), op) {}
 
::llvm::LogicalResult IncludeOpAdaptor::verify(::mlir::Location loc) {
  auto tblgen_arg_attrs = getProperties().arg_attrs; (void)tblgen_arg_attrs;
  auto tblgen_callee = getProperties().callee; (void)tblgen_callee;
  if (!tblgen_callee) return emitError(loc, "'verif.include' op requires attribute 'callee'");
  auto tblgen_mapOpGroupSizes = getProperties().mapOpGroupSizes; (void)tblgen_mapOpGroupSizes;
  if (!tblgen_mapOpGroupSizes) return emitError(loc, "'verif.include' op requires attribute 'mapOpGroupSizes'");
  auto tblgen_numDimsPerMap = getProperties().numDimsPerMap; (void)tblgen_numDimsPerMap;
  auto tblgen_res_attrs = getProperties().res_attrs; (void)tblgen_res_attrs;
  auto tblgen_templateParams = getProperties().templateParams; (void)tblgen_templateParams;
 
  if (tblgen_callee && !((::llvm::isa<::mlir::SymbolRefAttr>(tblgen_callee))))
    return emitError(loc, "'verif.include' op attribute 'callee' failed to satisfy constraint: symbol reference attribute");
 
  if (tblgen_templateParams && !((::llvm::isa<::mlir::ArrayAttr>(tblgen_templateParams))))
    return emitError(loc, "'verif.include' op attribute 'templateParams' failed to satisfy constraint: array attribute");
 
  if (tblgen_numDimsPerMap && !((::llvm::isa<::mlir::DenseI32ArrayAttr>(tblgen_numDimsPerMap))))
    return emitError(loc, "'verif.include' op attribute 'numDimsPerMap' failed to satisfy constraint: i32 dense array attribute");
 
  if (tblgen_mapOpGroupSizes && !((::llvm::isa<::mlir::DenseI32ArrayAttr>(tblgen_mapOpGroupSizes))))
    return emitError(loc, "'verif.include' op attribute 'mapOpGroupSizes' failed to satisfy constraint: i32 dense array attribute");
 
  if (tblgen_arg_attrs && !(((::llvm::isa<::mlir::ArrayAttr>(tblgen_arg_attrs))) && (::llvm::all_of(::llvm::cast<::mlir::ArrayAttr>(tblgen_arg_attrs), [&](::mlir::Attribute attr) { return attr && ((::llvm::isa<::mlir::DictionaryAttr>(attr))); }))))
    return emitError(loc, "'verif.include' op attribute 'arg_attrs' failed to satisfy constraint: Array of dictionary attributes");
 
  if (tblgen_res_attrs && !(((::llvm::isa<::mlir::ArrayAttr>(tblgen_res_attrs))) && (::llvm::all_of(::llvm::cast<::mlir::ArrayAttr>(tblgen_res_attrs), [&](::mlir::Attribute attr) { return attr && ((::llvm::isa<::mlir::DictionaryAttr>(attr))); }))))
    return emitError(loc, "'verif.include' op attribute 'res_attrs' failed to satisfy constraint: Array of dictionary attributes");
  return ::mlir::success();
}
 
std::pair<unsigned, unsigned> IncludeOp::getODSOperandIndexAndLength(unsigned index) {
  ::llvm::ArrayRef<int32_t> sizeAttr = getProperties().operandSegmentSizes;
 
  unsigned start = 0;
  for (unsigned i = 0; i < index; ++i)
    start += sizeAttr[i];
  return {start, sizeAttr[index]};
}
 
::mlir::MutableOperandRange IncludeOp::getArgOperandsMutable() {
  auto range = getODSOperandIndexAndLength(0);
  auto mutableRange = ::mlir::MutableOperandRange(getOperation(), range.first, range.second, ::mlir::MutableOperandRange::OperandSegment(0u, {getOperandSegmentSizesAttrName(), ::mlir::DenseI32ArrayAttr::get(getContext(), getProperties().operandSegmentSizes)}));
  return mutableRange;
}
 
::mlir::MutableOperandRangeRange IncludeOp::getMapOperandsMutable() {
  auto range = getODSOperandIndexAndLength(1);
  auto mutableRange = ::mlir::MutableOperandRange(getOperation(), range.first, range.second, ::mlir::MutableOperandRange::OperandSegment(1u, {getOperandSegmentSizesAttrName(), ::mlir::DenseI32ArrayAttr::get(getContext(), getProperties().operandSegmentSizes)}));
  return mutableRange.split(*(*this)->getAttrDictionary().getNamed(getMapOpGroupSizesAttrName()));
}
 
::llvm::LogicalResult IncludeOp::setPropertiesFromAttr(Properties &prop, ::mlir::Attribute attr, ::llvm::function_ref<::mlir::InFlightDiagnostic()> emitError) {
  ::mlir::DictionaryAttr dict = ::llvm::dyn_cast<::mlir::DictionaryAttr>(attr);
  if (!dict) {
    emitError() << "expected DictionaryAttr to set properties";
    return ::mlir::failure();
  }
 
  {
    auto &propStorage = prop.arg_attrs;
       auto attr = dict.get("arg_attrs");
    if (attr) {
      auto convertedAttr = ::llvm::dyn_cast<std::remove_reference_t<decltype(propStorage)>>(attr);
      if (convertedAttr) {
        propStorage = convertedAttr;
      } else {
        emitError() << "Invalid attribute `arg_attrs` in property conversion: " << attr;
        return ::mlir::failure();
      }
    }
  }
 
  {
    auto &propStorage = prop.callee;
       auto attr = dict.get("callee");
    if (attr) {
      auto convertedAttr = ::llvm::dyn_cast<std::remove_reference_t<decltype(propStorage)>>(attr);
      if (convertedAttr) {
        propStorage = convertedAttr;
      } else {
        emitError() << "Invalid attribute `callee` in property conversion: " << attr;
        return ::mlir::failure();
      }
    }
  }
 
  {
    auto &propStorage = prop.mapOpGroupSizes;
       auto attr = dict.get("mapOpGroupSizes");
    if (attr) {
      auto convertedAttr = ::llvm::dyn_cast<std::remove_reference_t<decltype(propStorage)>>(attr);
      if (convertedAttr) {
        propStorage = convertedAttr;
      } else {
        emitError() << "Invalid attribute `mapOpGroupSizes` in property conversion: " << attr;
        return ::mlir::failure();
      }
    }
  }
 
  {
    auto &propStorage = prop.numDimsPerMap;
       auto attr = dict.get("numDimsPerMap");
    if (attr) {
      auto convertedAttr = ::llvm::dyn_cast<std::remove_reference_t<decltype(propStorage)>>(attr);
      if (convertedAttr) {
        propStorage = convertedAttr;
      } else {
        emitError() << "Invalid attribute `numDimsPerMap` in property conversion: " << attr;
        return ::mlir::failure();
      }
    }
  }
 
  {
    auto &propStorage = prop.res_attrs;
       auto attr = dict.get("res_attrs");
    if (attr) {
      auto convertedAttr = ::llvm::dyn_cast<std::remove_reference_t<decltype(propStorage)>>(attr);
      if (convertedAttr) {
        propStorage = convertedAttr;
      } else {
        emitError() << "Invalid attribute `res_attrs` in property conversion: " << attr;
        return ::mlir::failure();
      }
    }
  }
 
  {
    auto &propStorage = prop.templateParams;
       auto attr = dict.get("templateParams");
    if (attr) {
      auto convertedAttr = ::llvm::dyn_cast<std::remove_reference_t<decltype(propStorage)>>(attr);
      if (convertedAttr) {
        propStorage = convertedAttr;
      } else {
        emitError() << "Invalid attribute `templateParams` in property conversion: " << attr;
        return ::mlir::failure();
      }
    }
  }
{
 
      auto setFromAttr = [] (auto &propStorage, ::mlir::Attribute propAttr,
               ::llvm::function_ref<::mlir::InFlightDiagnostic()> emitError) -> ::mlir::LogicalResult {
        return convertFromAttribute(propStorage, propAttr, emitError);
      };
         auto attr = dict.get("operandSegmentSizes");   if (!attr) attr = dict.get("operand_segment_sizes");;
;
      if (attr && ::mlir::failed(setFromAttr(prop.operandSegmentSizes, attr, [&]() {
            return emitError() << "for `operandSegmentSizes`: ";
          })))
        return ::mlir::failure();
  }
  return ::mlir::success();
}
 
::mlir::Attribute IncludeOp::getPropertiesAsAttr(::mlir::MLIRContext *ctx, const Properties &prop) {
    ::mlir::SmallVector<::mlir::NamedAttribute> attrs;
    ::mlir::Builder odsBuilder{ctx};
 
    {
      const auto &propStorage = prop.arg_attrs;
      if (propStorage)
        attrs.push_back(odsBuilder.getNamedAttr("arg_attrs",
                                       propStorage));
    }
 
    {
      const auto &propStorage = prop.callee;
      if (propStorage)
        attrs.push_back(odsBuilder.getNamedAttr("callee",
                                       propStorage));
    }
 
    {
      const auto &propStorage = prop.mapOpGroupSizes;
      if (propStorage)
        attrs.push_back(odsBuilder.getNamedAttr("mapOpGroupSizes",
                                       propStorage));
    }
 
    {
      const auto &propStorage = prop.numDimsPerMap;
      if (propStorage)
        attrs.push_back(odsBuilder.getNamedAttr("numDimsPerMap",
                                       propStorage));
    }
 
    {
      const auto &propStorage = prop.res_attrs;
      if (propStorage)
        attrs.push_back(odsBuilder.getNamedAttr("res_attrs",
                                       propStorage));
    }
 
    {
      const auto &propStorage = prop.templateParams;
      if (propStorage)
        attrs.push_back(odsBuilder.getNamedAttr("templateParams",
                                       propStorage));
    }
 
    {
      const auto &propStorage = prop.operandSegmentSizes;
      auto attr = [&]() -> ::mlir::Attribute {
        return ::mlir::DenseI32ArrayAttr::get(ctx, propStorage);
      }();
      attrs.push_back(odsBuilder.getNamedAttr("operandSegmentSizes", attr));
    }
 
  if (!attrs.empty())
    return odsBuilder.getDictionaryAttr(attrs);
  return {};
}
 
llvm::hash_code IncludeOp::computePropertiesHash(const Properties &prop) {
  auto hash_operandSegmentSizes_ = [] (const auto &propStorage) -> llvm::hash_code {
    using ::llvm::hash_value;
    return ::llvm::hash_combine_range(std::begin(propStorage), std::end(propStorage));;
  };
  using llvm::hash_value;
  return llvm::hash_combine(
    llvm::hash_value(prop.arg_attrs.getAsOpaquePointer()), 
    llvm::hash_value(prop.callee.getAsOpaquePointer()), 
    llvm::hash_value(prop.mapOpGroupSizes.getAsOpaquePointer()), 
    llvm::hash_value(prop.numDimsPerMap.getAsOpaquePointer()), 
    llvm::hash_value(prop.res_attrs.getAsOpaquePointer()), 
    llvm::hash_value(prop.templateParams.getAsOpaquePointer()), 
    hash_operandSegmentSizes_(prop.operandSegmentSizes));
}
 
std::optional<mlir::Attribute> IncludeOp::getInherentAttr(::mlir::MLIRContext *ctx, const Properties &prop, llvm::StringRef name) {
    if (name == "arg_attrs")
      return prop.arg_attrs;
 
    if (name == "callee")
      return prop.callee;
 
    if (name == "mapOpGroupSizes")
      return prop.mapOpGroupSizes;
 
    if (name == "numDimsPerMap")
      return prop.numDimsPerMap;
 
    if (name == "res_attrs")
      return prop.res_attrs;
 
    if (name == "templateParams")
      return prop.templateParams;
    if (name == "operand_segment_sizes" || name == "operandSegmentSizes") return [&]() -> ::mlir::Attribute { return ::mlir::DenseI32ArrayAttr::get(ctx, prop.operandSegmentSizes); }();
  return std::nullopt;
}
 
void IncludeOp::setInherentAttr(Properties &prop, llvm::StringRef name, mlir::Attribute value) {
    if (name == "arg_attrs") {
       prop.arg_attrs = ::llvm::dyn_cast_or_null<std::remove_reference_t<decltype(prop.arg_attrs)>>(value);
       return;
    }
 
    if (name == "callee") {
       prop.callee = ::llvm::dyn_cast_or_null<std::remove_reference_t<decltype(prop.callee)>>(value);
       return;
    }
 
    if (name == "mapOpGroupSizes") {
       prop.mapOpGroupSizes = ::llvm::dyn_cast_or_null<std::remove_reference_t<decltype(prop.mapOpGroupSizes)>>(value);
       return;
    }
 
    if (name == "numDimsPerMap") {
       prop.numDimsPerMap = ::llvm::dyn_cast_or_null<std::remove_reference_t<decltype(prop.numDimsPerMap)>>(value);
       return;
    }
 
    if (name == "res_attrs") {
       prop.res_attrs = ::llvm::dyn_cast_or_null<std::remove_reference_t<decltype(prop.res_attrs)>>(value);
       return;
    }
 
    if (name == "templateParams") {
       prop.templateParams = ::llvm::dyn_cast_or_null<std::remove_reference_t<decltype(prop.templateParams)>>(value);
       return;
    }
        if (name == "operand_segment_sizes" || name == "operandSegmentSizes") {
       auto arrAttr = ::llvm::dyn_cast_or_null<::mlir::DenseI32ArrayAttr>(value);
       if (!arrAttr) return;
       if (arrAttr.size() != sizeof(prop.operandSegmentSizes) / sizeof(int32_t))
         return;
       llvm::copy(arrAttr.asArrayRef(), prop.operandSegmentSizes.begin());
       return;
    }
}
 
void IncludeOp::populateInherentAttrs(::mlir::MLIRContext *ctx, const Properties &prop, ::mlir::NamedAttrList &attrs) {
    if (prop.arg_attrs) attrs.append("arg_attrs", prop.arg_attrs);
 
    if (prop.callee) attrs.append("callee", prop.callee);
 
    if (prop.mapOpGroupSizes) attrs.append("mapOpGroupSizes", prop.mapOpGroupSizes);
 
    if (prop.numDimsPerMap) attrs.append("numDimsPerMap", prop.numDimsPerMap);
 
    if (prop.res_attrs) attrs.append("res_attrs", prop.res_attrs);
 
    if (prop.templateParams) attrs.append("templateParams", prop.templateParams);
  attrs.append("operandSegmentSizes", [&]() -> ::mlir::Attribute { return ::mlir::DenseI32ArrayAttr::get(ctx, prop.operandSegmentSizes); }());
}
 
::llvm::LogicalResult IncludeOp::verifyInherentAttrs(::mlir::OperationName opName, ::mlir::NamedAttrList &attrs, llvm::function_ref<::mlir::InFlightDiagnostic()> emitError) {
    {
      ::mlir::Attribute attr = attrs.get(getArgAttrsAttrName(opName));
      if (attr && ::mlir::failed(__mlir_ods_local_attr_constraint_Ops4(attr, "arg_attrs", emitError)))
        return ::mlir::failure();
    }
 
    {
      ::mlir::Attribute attr = attrs.get(getCalleeAttrName(opName));
      if (attr && ::mlir::failed(__mlir_ods_local_attr_constraint_Ops2(attr, "callee", emitError)))
        return ::mlir::failure();
    }
 
    {
      ::mlir::Attribute attr = attrs.get(getMapOpGroupSizesAttrName(opName));
      if (attr && ::mlir::failed(__mlir_ods_local_attr_constraint_Ops6(attr, "mapOpGroupSizes", emitError)))
        return ::mlir::failure();
    }
 
    {
      ::mlir::Attribute attr = attrs.get(getNumDimsPerMapAttrName(opName));
      if (attr && ::mlir::failed(__mlir_ods_local_attr_constraint_Ops6(attr, "numDimsPerMap", emitError)))
        return ::mlir::failure();
    }
 
    {
      ::mlir::Attribute attr = attrs.get(getResAttrsAttrName(opName));
      if (attr && ::mlir::failed(__mlir_ods_local_attr_constraint_Ops4(attr, "res_attrs", emitError)))
        return ::mlir::failure();
    }
 
    {
      ::mlir::Attribute attr = attrs.get(getTemplateParamsAttrName(opName));
      if (attr && ::mlir::failed(__mlir_ods_local_attr_constraint_Ops5(attr, "templateParams", emitError)))
        return ::mlir::failure();
    }
    return ::mlir::success();
}
 
::llvm::LogicalResult IncludeOp::readProperties(::mlir::DialectBytecodeReader &reader, ::mlir::OperationState &state) {
  auto &prop = state.getOrAddProperties<Properties>(); (void)prop;
  if (::mlir::failed(reader.readOptionalAttribute(prop.arg_attrs)))
    return ::mlir::failure();
 
  if (::mlir::failed(reader.readAttribute(prop.callee)))
    return ::mlir::failure();
 
  if (::mlir::failed(reader.readAttribute(prop.mapOpGroupSizes)))
    return ::mlir::failure();
 
  if (::mlir::failed(reader.readOptionalAttribute(prop.numDimsPerMap)))
    return ::mlir::failure();
 
  if (reader.getBytecodeVersion() < /*kNativePropertiesODSSegmentSize=*/6) {
    auto &propStorage = prop.operandSegmentSizes;
    ::mlir::DenseI32ArrayAttr attr;
    if (::mlir::failed(reader.readAttribute(attr))) return ::mlir::failure();
    if (attr.size() > static_cast<int64_t>(sizeof(propStorage) / sizeof(int32_t))) {
      reader.emitError("size mismatch for operand/result_segment_size");
      return ::mlir::failure();
    }
    ::llvm::copy(::llvm::ArrayRef<int32_t>(attr), propStorage.begin());
  }
 
  if (::mlir::failed(reader.readOptionalAttribute(prop.res_attrs)))
    return ::mlir::failure();
 
  if (::mlir::failed(reader.readOptionalAttribute(prop.templateParams)))
    return ::mlir::failure();
 
  {
    auto &propStorage = prop.operandSegmentSizes;
    auto readProp = [&]() {
 
  if (reader.getBytecodeVersion() >= /*kNativePropertiesODSSegmentSize=*/6)
    return reader.readSparseArray(::llvm::MutableArrayRef(propStorage));
;
      return ::mlir::success();
    };
    if (::mlir::failed(readProp()))
      return ::mlir::failure();
  }
  return ::mlir::success();
}
 
void IncludeOp::writeProperties(::mlir::DialectBytecodeWriter &writer) {
  auto &prop = getProperties(); (void)prop;
 
  writer.writeOptionalAttribute(prop.arg_attrs);
  writer.writeAttribute(prop.callee);
  writer.writeAttribute(prop.mapOpGroupSizes);
 
  writer.writeOptionalAttribute(prop.numDimsPerMap);
 
if (writer.getBytecodeVersion() < /*kNativePropertiesODSSegmentSize=*/6) {
  auto &propStorage = prop.operandSegmentSizes;
  writer.writeAttribute(::mlir::DenseI32ArrayAttr::get(this->getContext(), propStorage));
}
 
  writer.writeOptionalAttribute(prop.res_attrs);
 
  writer.writeOptionalAttribute(prop.templateParams);
 
  {
    auto &propStorage = prop.operandSegmentSizes;
 
  if (writer.getBytecodeVersion() >= /*kNativePropertiesODSSegmentSize=*/6)
    writer.writeSparseArray(::llvm::ArrayRef(propStorage));
;
  }
}
 
::mlir::SymbolRefAttr IncludeOp::getCallee() {
  auto attr = getCalleeAttr();
  return attr;
}
 
::std::optional< ::mlir::ArrayAttr > IncludeOp::getTemplateParams() {
  auto attr = getTemplateParamsAttr();
  return attr ? ::std::optional< ::mlir::ArrayAttr >(attr) : (::std::nullopt);
}
 
::llvm::ArrayRef<int32_t> IncludeOp::getNumDimsPerMap() {
  auto attr = getNumDimsPerMapAttr();
  return attr;
}
 
::llvm::ArrayRef<int32_t> IncludeOp::getMapOpGroupSizes() {
  auto attr = getMapOpGroupSizesAttr();
  return attr;
}
 
::std::optional< ::mlir::ArrayAttr > IncludeOp::getArgAttrs() {
  auto attr = getArgAttrsAttr();
  return attr ? ::std::optional< ::mlir::ArrayAttr >(attr) : (::std::nullopt);
}
 
::std::optional< ::mlir::ArrayAttr > IncludeOp::getResAttrs() {
  auto attr = getResAttrsAttr();
  return attr ? ::std::optional< ::mlir::ArrayAttr >(attr) : (::std::nullopt);
}
 
void IncludeOp::setNumDimsPerMap(::llvm::ArrayRef<int32_t> attrValue) {
  getProperties().numDimsPerMap = ::mlir::Builder((*this)->getContext()).getDenseI32ArrayAttr(attrValue);
}
 
void IncludeOp::setMapOpGroupSizes(::llvm::ArrayRef<int32_t> attrValue) {
  getProperties().mapOpGroupSizes = ::mlir::Builder((*this)->getContext()).getDenseI32ArrayAttr(attrValue);
}
 
IncludeOp IncludeOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::SymbolRefAttr callee, ::mlir::ValueRange argOperands, ::llvm::ArrayRef<::mlir::Attribute> templateParams) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(callee)>(callee), std::forward<decltype(argOperands)>(argOperands), std::forward<decltype(templateParams)>(templateParams));
  auto __res__ = ::llvm::dyn_cast<IncludeOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
IncludeOp IncludeOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::SymbolRefAttr callee, ::mlir::ValueRange argOperands, ::llvm::ArrayRef<::mlir::Attribute> templateParams) {
  return create(builder, builder.getLoc(), std::forward<decltype(callee)>(callee), std::forward<decltype(argOperands)>(argOperands), std::forward<decltype(templateParams)>(templateParams));
}
 
IncludeOp IncludeOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::SymbolRefAttr callee, ::llvm::ArrayRef<::mlir::ValueRange> mapOperands, ::mlir::DenseI32ArrayAttr numDimsPerMap, ::mlir::ValueRange argOperands, ::llvm::ArrayRef<::mlir::Attribute> templateParams) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(callee)>(callee), std::forward<decltype(mapOperands)>(mapOperands), std::forward<decltype(numDimsPerMap)>(numDimsPerMap), std::forward<decltype(argOperands)>(argOperands), std::forward<decltype(templateParams)>(templateParams));
  auto __res__ = ::llvm::dyn_cast<IncludeOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
IncludeOp IncludeOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::SymbolRefAttr callee, ::llvm::ArrayRef<::mlir::ValueRange> mapOperands, ::mlir::DenseI32ArrayAttr numDimsPerMap, ::mlir::ValueRange argOperands, ::llvm::ArrayRef<::mlir::Attribute> templateParams) {
  return create(builder, builder.getLoc(), std::forward<decltype(callee)>(callee), std::forward<decltype(mapOperands)>(mapOperands), std::forward<decltype(numDimsPerMap)>(numDimsPerMap), std::forward<decltype(argOperands)>(argOperands), std::forward<decltype(templateParams)>(templateParams));
}
 
void IncludeOp::build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, ::mlir::SymbolRefAttr callee, ::llvm::ArrayRef<::mlir::ValueRange> mapOperands, ::llvm::ArrayRef<int32_t> numDimsPerMap, ::mlir::ValueRange argOperands, ::llvm::ArrayRef<::mlir::Attribute> templateParams) {
                    build(odsBuilder, odsState, callee, mapOperands,
                          odsBuilder.getDenseI32ArrayAttr(numDimsPerMap),
                          argOperands, templateParams);
                  
}
 
IncludeOp IncludeOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::SymbolRefAttr callee, ::llvm::ArrayRef<::mlir::ValueRange> mapOperands, ::llvm::ArrayRef<int32_t> numDimsPerMap, ::mlir::ValueRange argOperands, ::llvm::ArrayRef<::mlir::Attribute> templateParams) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(callee)>(callee), std::forward<decltype(mapOperands)>(mapOperands), std::forward<decltype(numDimsPerMap)>(numDimsPerMap), std::forward<decltype(argOperands)>(argOperands), std::forward<decltype(templateParams)>(templateParams));
  auto __res__ = ::llvm::dyn_cast<IncludeOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
IncludeOp IncludeOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::SymbolRefAttr callee, ::llvm::ArrayRef<::mlir::ValueRange> mapOperands, ::llvm::ArrayRef<int32_t> numDimsPerMap, ::mlir::ValueRange argOperands, ::llvm::ArrayRef<::mlir::Attribute> templateParams) {
  return create(builder, builder.getLoc(), std::forward<decltype(callee)>(callee), std::forward<decltype(mapOperands)>(mapOperands), std::forward<decltype(numDimsPerMap)>(numDimsPerMap), std::forward<decltype(argOperands)>(argOperands), std::forward<decltype(templateParams)>(templateParams));
}
 
void IncludeOp::build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, ::llzk::verif::ContractOp callee, ::mlir::ValueRange argOperands, ::llvm::ArrayRef<::mlir::Attribute> templateParams) {
                    build(odsBuilder, odsState,
                          callee.getFullyQualifiedName(false),
                          argOperands, templateParams);
                  
}
 
IncludeOp IncludeOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::llzk::verif::ContractOp callee, ::mlir::ValueRange argOperands, ::llvm::ArrayRef<::mlir::Attribute> templateParams) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(callee)>(callee), std::forward<decltype(argOperands)>(argOperands), std::forward<decltype(templateParams)>(templateParams));
  auto __res__ = ::llvm::dyn_cast<IncludeOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
IncludeOp IncludeOp::create(::mlir::ImplicitLocOpBuilder &builder, ::llzk::verif::ContractOp callee, ::mlir::ValueRange argOperands, ::llvm::ArrayRef<::mlir::Attribute> templateParams) {
  return create(builder, builder.getLoc(), std::forward<decltype(callee)>(callee), std::forward<decltype(argOperands)>(argOperands), std::forward<decltype(templateParams)>(templateParams));
}
 
void IncludeOp::build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, ::llzk::verif::ContractOp callee, ::llvm::ArrayRef<::mlir::ValueRange> mapOperands, ::mlir::DenseI32ArrayAttr numDimsPerMap, ::mlir::ValueRange argOperands, ::llvm::ArrayRef<::mlir::Attribute> templateParams) {
                    build(odsBuilder, odsState,
                          callee.getFullyQualifiedName(false), mapOperands, numDimsPerMap,
                          argOperands, templateParams);
                  
}
 
IncludeOp IncludeOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::llzk::verif::ContractOp callee, ::llvm::ArrayRef<::mlir::ValueRange> mapOperands, ::mlir::DenseI32ArrayAttr numDimsPerMap, ::mlir::ValueRange argOperands, ::llvm::ArrayRef<::mlir::Attribute> templateParams) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(callee)>(callee), std::forward<decltype(mapOperands)>(mapOperands), std::forward<decltype(numDimsPerMap)>(numDimsPerMap), std::forward<decltype(argOperands)>(argOperands), std::forward<decltype(templateParams)>(templateParams));
  auto __res__ = ::llvm::dyn_cast<IncludeOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
IncludeOp IncludeOp::create(::mlir::ImplicitLocOpBuilder &builder, ::llzk::verif::ContractOp callee, ::llvm::ArrayRef<::mlir::ValueRange> mapOperands, ::mlir::DenseI32ArrayAttr numDimsPerMap, ::mlir::ValueRange argOperands, ::llvm::ArrayRef<::mlir::Attribute> templateParams) {
  return create(builder, builder.getLoc(), std::forward<decltype(callee)>(callee), std::forward<decltype(mapOperands)>(mapOperands), std::forward<decltype(numDimsPerMap)>(numDimsPerMap), std::forward<decltype(argOperands)>(argOperands), std::forward<decltype(templateParams)>(templateParams));
}
 
void IncludeOp::build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, ::llzk::verif::ContractOp callee, ::llvm::ArrayRef<::mlir::ValueRange> mapOperands, ::llvm::ArrayRef<int32_t> numDimsPerMap, ::mlir::ValueRange argOperands, ::llvm::ArrayRef<::mlir::Attribute> templateParams) {
                    build(odsBuilder, odsState, callee, mapOperands,
                          odsBuilder.getDenseI32ArrayAttr(numDimsPerMap),
                          argOperands, templateParams);
                  
}
 
IncludeOp IncludeOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::llzk::verif::ContractOp callee, ::llvm::ArrayRef<::mlir::ValueRange> mapOperands, ::llvm::ArrayRef<int32_t> numDimsPerMap, ::mlir::ValueRange argOperands, ::llvm::ArrayRef<::mlir::Attribute> templateParams) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(callee)>(callee), std::forward<decltype(mapOperands)>(mapOperands), std::forward<decltype(numDimsPerMap)>(numDimsPerMap), std::forward<decltype(argOperands)>(argOperands), std::forward<decltype(templateParams)>(templateParams));
  auto __res__ = ::llvm::dyn_cast<IncludeOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
IncludeOp IncludeOp::create(::mlir::ImplicitLocOpBuilder &builder, ::llzk::verif::ContractOp callee, ::llvm::ArrayRef<::mlir::ValueRange> mapOperands, ::llvm::ArrayRef<int32_t> numDimsPerMap, ::mlir::ValueRange argOperands, ::llvm::ArrayRef<::mlir::Attribute> templateParams) {
  return create(builder, builder.getLoc(), std::forward<decltype(callee)>(callee), std::forward<decltype(mapOperands)>(mapOperands), std::forward<decltype(numDimsPerMap)>(numDimsPerMap), std::forward<decltype(argOperands)>(argOperands), std::forward<decltype(templateParams)>(templateParams));
}
 
void IncludeOp::populateDefaultProperties(::mlir::OperationName opName, Properties &properties) {
  ::mlir::Builder odsBuilder(opName.getContext());
  if (!properties.numDimsPerMap)
    properties.numDimsPerMap = odsBuilder.getDenseI32ArrayAttr({});
}
 
::llvm::LogicalResult IncludeOp::verifyInvariantsImpl() {
  auto tblgen_arg_attrs = getProperties().arg_attrs; (void)tblgen_arg_attrs;
  auto tblgen_callee = getProperties().callee; (void)tblgen_callee;
  if (!tblgen_callee) return emitOpError("requires attribute 'callee'");
  auto tblgen_mapOpGroupSizes = getProperties().mapOpGroupSizes; (void)tblgen_mapOpGroupSizes;
  if (!tblgen_mapOpGroupSizes) return emitOpError("requires attribute 'mapOpGroupSizes'");
  auto tblgen_numDimsPerMap = getProperties().numDimsPerMap; (void)tblgen_numDimsPerMap;
  auto tblgen_res_attrs = getProperties().res_attrs; (void)tblgen_res_attrs;
  auto tblgen_templateParams = getProperties().templateParams; (void)tblgen_templateParams;
 
  if (::mlir::failed(__mlir_ods_local_attr_constraint_Ops2(*this, tblgen_callee, "callee")))
    return ::mlir::failure();
 
  if (::mlir::failed(__mlir_ods_local_attr_constraint_Ops5(*this, tblgen_templateParams, "templateParams")))
    return ::mlir::failure();
 
  if (::mlir::failed(__mlir_ods_local_attr_constraint_Ops6(*this, tblgen_numDimsPerMap, "numDimsPerMap")))
    return ::mlir::failure();
 
  if (::mlir::failed(__mlir_ods_local_attr_constraint_Ops6(*this, tblgen_mapOpGroupSizes, "mapOpGroupSizes")))
    return ::mlir::failure();
 
  if (::mlir::failed(__mlir_ods_local_attr_constraint_Ops4(*this, tblgen_arg_attrs, "arg_attrs")))
    return ::mlir::failure();
 
  if (::mlir::failed(__mlir_ods_local_attr_constraint_Ops4(*this, tblgen_res_attrs, "res_attrs")))
    return ::mlir::failure();
  {
    unsigned index = 0; (void)index;
    auto valueGroup0 = getODSOperands(0);
 
    for (auto v : valueGroup0) {
      if (::mlir::failed(__mlir_ods_local_type_constraint_Ops4(*this, v.getType(), "operand", index++)))
        return ::mlir::failure();
    }
    auto valueGroup1 = getODSOperands(1);
    if (::mlir::failed(::mlir::OpTrait::impl::verifyValueSizeAttr(*this, "mapOpGroupSizes", "mapOperands", valueGroup1.size())))
      return ::mlir::failure();
 
    for (auto v : valueGroup1) {
      if (::mlir::failed(__mlir_ods_local_type_constraint_Ops5(*this, v.getType(), "operand", index++)))
        return ::mlir::failure();
    }
  }
  return ::mlir::success();
}
 
::llvm::LogicalResult IncludeOp::verifyInvariants() {
  return verifyInvariantsImpl();
}
 
::mlir::ParseResult IncludeOp::parse(::mlir::OpAsmParser &parser, ::mlir::OperationState &result) {
  ::mlir::SymbolRefAttr calleeAttr;
  ::mlir::ArrayAttr templateParamsAttr;
  ::llvm::SmallVector<::mlir::OpAsmParser::UnresolvedOperand, 4> argOperandsOperands;
  ::llvm::SMLoc argOperandsOperandsLoc;
  (void)argOperandsOperandsLoc;
  ::llvm::SmallVector<::mlir::OpAsmParser::UnresolvedOperand, 4> mapOperandsOperands;
    llvm::SmallVector<int32_t> mapOperandsOperandGroupSizes;
  ::llvm::SMLoc mapOperandsOperandsLoc;
  (void)mapOperandsOperandsLoc;
  ::mlir::DenseI32ArrayAttr numDimsPerMapAttr;
  ::llvm::ArrayRef<::mlir::Type> argOperandsTypes;
  ::llvm::ArrayRef<::mlir::Type> allResultTypes;
 
  if (parser.parseCustomAttributeWithFallback(calleeAttr, parser.getBuilder().getType<::mlir::NoneType>())) {
    return ::mlir::failure();
  }
  if (calleeAttr) result.getOrAddProperties<IncludeOp::Properties>().callee = calleeAttr;
  if (::mlir::succeeded(parser.parseOptionalLess())) {
  {
    auto odsResult = parseTemplateParams(parser, templateParamsAttr);
    if (odsResult) return ::mlir::failure();
    if (templateParamsAttr)
      result.getOrAddProperties<IncludeOp::Properties>().templateParams = templateParamsAttr;
  }
  if (parser.parseGreater())
    return ::mlir::failure();
  }
  if (parser.parseLParen())
    return ::mlir::failure();
 
  argOperandsOperandsLoc = parser.getCurrentLocation();
  if (parser.parseOperandList(argOperandsOperands))
    return ::mlir::failure();
  if (parser.parseRParen())
    return ::mlir::failure();
  if (::mlir::succeeded(parser.parseOptionalLBrace())) {
  {
    mapOperandsOperandsLoc = parser.getCurrentLocation();
    ::llvm::SmallVector<::llvm::SmallVector<::mlir::OpAsmParser::UnresolvedOperand>> mapOperandsOperandGroups;
    auto odsResult = parseMultiDimAndSymbolList(parser, mapOperandsOperandGroups, numDimsPerMapAttr);
    if (odsResult) return ::mlir::failure();
    for (const auto &subRange : mapOperandsOperandGroups) {
      mapOperandsOperands.append(subRange.begin(), subRange.end());
      mapOperandsOperandGroupSizes.push_back(subRange.size());
    }
    if (numDimsPerMapAttr)
      result.getOrAddProperties<IncludeOp::Properties>().numDimsPerMap = numDimsPerMapAttr;
  }
  if (parser.parseRBrace())
    return ::mlir::failure();
  }
  if (parser.parseColon())
    return ::mlir::failure();
 
  ::mlir::FunctionType argOperands__allResult_functionType;
  if (parser.parseType(argOperands__allResult_functionType))
    return ::mlir::failure();
  argOperandsTypes = argOperands__allResult_functionType.getInputs();
  allResultTypes = argOperands__allResult_functionType.getResults();
  {
    auto odsResult = parseAttrDictWithWarnings(parser, result.attributes, result);
    if (odsResult) return ::mlir::failure();
  }
::llvm::copy(::llvm::ArrayRef<int32_t>({static_cast<int32_t>(argOperandsOperands.size()), static_cast<int32_t>(mapOperandsOperands.size())}), result.getOrAddProperties<IncludeOp::Properties>().operandSegmentSizes.begin());
  result.getOrAddProperties<IncludeOp::Properties>().mapOpGroupSizes = parser.getBuilder().getDenseI32ArrayAttr(mapOperandsOperandGroupSizes);
  ::mlir::Type odsBuildableType0 = parser.getBuilder().getIndexType();
  result.addTypes(allResultTypes);
  if (parser.resolveOperands(argOperandsOperands, argOperandsTypes, argOperandsOperandsLoc, result.operands))
    return ::mlir::failure();
  if (parser.resolveOperands(mapOperandsOperands, odsBuildableType0, mapOperandsOperandsLoc, result.operands))
    return ::mlir::failure();
  return ::mlir::success();
}
 
::llvm::LogicalResult IncludeOp::setPropertiesFromParsedAttr(Properties &prop, ::mlir::Attribute attr, ::llvm::function_ref<::mlir::InFlightDiagnostic()> emitError) {
  ::mlir::DictionaryAttr dict = ::llvm::dyn_cast<::mlir::DictionaryAttr>(attr);
  if (!dict) {
    emitError() << "expected DictionaryAttr to set properties";
    return ::mlir::failure();
  }
  // keep track of used keys in the input dictionary to be able to error out
  // if there are some unknown ones.
  ::mlir::DenseSet<::mlir::StringAttr> usedKeys;
  ::mlir::MLIRContext *ctx = dict.getContext();
  (void)ctx;
  {
 
    auto &propStorage = prop.mapOpGroupSizes;
    auto mapOpGroupSizesAttrName = ::mlir::StringAttr::get(ctx, "mapOpGroupSizes");
    auto attr = dict.get(mapOpGroupSizesAttrName);
    usedKeys.insert(mapOpGroupSizesAttrName);
    if (attr || /*isRequired=*/true) {
      if (!attr) {
        emitError() << "expected key entry for mapOpGroupSizes in DictionaryAttr to set "
                   "Properties.";
        return ::mlir::failure();
      }
      auto convertedAttr = ::llvm::dyn_cast<std::remove_reference_t<decltype(propStorage)>>(attr);
      if (convertedAttr) {
        propStorage = convertedAttr;
      } else {
        emitError() << "Invalid attribute `mapOpGroupSizes` in property conversion: " << attr;
        return ::mlir::failure();
      }
    }
  }
  {
 
    auto &propStorage = prop.arg_attrs;
    auto arg_attrsAttrName = ::mlir::StringAttr::get(ctx, "arg_attrs");
    auto attr = dict.get(arg_attrsAttrName);
    usedKeys.insert(arg_attrsAttrName);
    if (attr || /*isRequired=*/false) {
      if (!attr) {
        emitError() << "expected key entry for arg_attrs in DictionaryAttr to set "
                   "Properties.";
        return ::mlir::failure();
      }
      auto convertedAttr = ::llvm::dyn_cast<std::remove_reference_t<decltype(propStorage)>>(attr);
      if (convertedAttr) {
        propStorage = convertedAttr;
      } else {
        emitError() << "Invalid attribute `arg_attrs` in property conversion: " << attr;
        return ::mlir::failure();
      }
    }
  }
  {
 
    auto &propStorage = prop.res_attrs;
    auto res_attrsAttrName = ::mlir::StringAttr::get(ctx, "res_attrs");
    auto attr = dict.get(res_attrsAttrName);
    usedKeys.insert(res_attrsAttrName);
    if (attr || /*isRequired=*/false) {
      if (!attr) {
        emitError() << "expected key entry for res_attrs in DictionaryAttr to set "
                   "Properties.";
        return ::mlir::failure();
      }
      auto convertedAttr = ::llvm::dyn_cast<std::remove_reference_t<decltype(propStorage)>>(attr);
      if (convertedAttr) {
        propStorage = convertedAttr;
      } else {
        emitError() << "Invalid attribute `res_attrs` in property conversion: " << attr;
        return ::mlir::failure();
      }
    }
  }
 
  for (::mlir::NamedAttribute attr : dict) {
    if (!usedKeys.contains(attr.getName()))
      return emitError() << "unknown key '" << attr.getName() <<
          "' when parsing properties dictionary";
  }
  return ::mlir::success();
}
 
void IncludeOp::print(::mlir::OpAsmPrinter &_odsPrinter) {
  _odsPrinter << ' ';
  _odsPrinter.printAttributeWithoutType(getCalleeAttr());
  if (((getTemplateParamsAttr()))) {
    _odsPrinter << "<";
    printTemplateParams(_odsPrinter, *this, getTemplateParamsAttr());
    _odsPrinter << ">";
  }
  _odsPrinter << "(";
  _odsPrinter << getArgOperands();
  _odsPrinter << ")";
  if (((!getMapOperands().empty()) || (getNumDimsPerMapAttr() != ::mlir::OpBuilder((*this)->getContext()).getDenseI32ArrayAttr({})))) {
    _odsPrinter << ' ' << "{";
    printMultiDimAndSymbolList(_odsPrinter, *this, getMapOperands(), getNumDimsPerMapAttr());
    _odsPrinter << "}";
  }
  _odsPrinter << ' ' << ":";
  _odsPrinter << ' ';
  _odsPrinter.printFunctionalType(getArgOperands().getTypes(), getOperation()->getResultTypes());
  _odsPrinter << ' ';
  printAttrDictWithWarnings(_odsPrinter, *this, getOperation()->getAttrDictionary(), getProperties());
}
 
 
} // namespace llzk::verif
MLIR_DEFINE_EXPLICIT_TYPE_ID(::llzk::verif::IncludeOp)
MLIR_DEFINE_EXPLICIT_TYPE_ID(::llzk::verif::detail::IncludeOpGenericAdaptorBase::Properties)
 
namespace llzk::verif {
 
 
//===----------------------------------------------------------------------===//
// ::llzk::verif::IncreasesOp definitions
//===----------------------------------------------------------------------===//
 
namespace detail {
 
IncreasesOpGenericAdaptorBase::IncreasesOpGenericAdaptorBase(IncreasesOp op) : odsAttrs(op->getRawDictionaryAttrs()), odsOpName(op->getName()), properties(op.getProperties()), odsRegions(op->getRegions()) {}
 
 
} // namespace detail
IncreasesOpAdaptor::IncreasesOpAdaptor(IncreasesOp op) : IncreasesOpGenericAdaptor(op->getOperands(), op) {}
 
::llvm::LogicalResult IncreasesOpAdaptor::verify(::mlir::Location loc) {
  return ::mlir::success();
}
 
::llvm::LogicalResult IncreasesOp::setPropertiesFromAttr(Properties &prop, ::mlir::Attribute attr, ::llvm::function_ref<::mlir::InFlightDiagnostic()> emitError) {
  ::mlir::DictionaryAttr dict = ::llvm::dyn_cast<::mlir::DictionaryAttr>(attr);
  if (!dict) {
    emitError() << "expected DictionaryAttr to set properties";
    return ::mlir::failure();
  }
      return ::mlir::success();
}
 
::mlir::Attribute IncreasesOp::getPropertiesAsAttr(::mlir::MLIRContext *ctx, const Properties &prop) {
    ::mlir::SmallVector<::mlir::NamedAttribute> attrs;
    ::mlir::Builder odsBuilder{ctx};
 
  if (!attrs.empty())
    return odsBuilder.getDictionaryAttr(attrs);
  return {};
}
 
llvm::hash_code IncreasesOp::computePropertiesHash(const Properties &prop) {
  using llvm::hash_value;
  return llvm::hash_combine();
}
 
std::optional<mlir::Attribute> IncreasesOp::getInherentAttr(::mlir::MLIRContext *ctx, const Properties &prop, llvm::StringRef name) {
  return std::nullopt;
}
 
void IncreasesOp::setInherentAttr(Properties &prop, llvm::StringRef name, mlir::Attribute value) {
}
 
void IncreasesOp::populateInherentAttrs(::mlir::MLIRContext *ctx, const Properties &prop, ::mlir::NamedAttrList &attrs) {
}
 
::llvm::LogicalResult IncreasesOp::verifyInherentAttrs(::mlir::OperationName opName, ::mlir::NamedAttrList &attrs, llvm::function_ref<::mlir::InFlightDiagnostic()> emitError) {
    return ::mlir::success();
}
 
void IncreasesOp::build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, ::mlir::Value value) {
  odsState.addOperands(value);
}
 
IncreasesOp IncreasesOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::Value value) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(value)>(value));
  auto __res__ = ::llvm::dyn_cast<IncreasesOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
IncreasesOp IncreasesOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::Value value) {
  return create(builder, builder.getLoc(), std::forward<decltype(value)>(value));
}
 
void IncreasesOp::build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, ::mlir::TypeRange resultTypes, ::mlir::Value value) {
  odsState.addOperands(value);
  assert(resultTypes.size() == 0u && "mismatched number of results");
  odsState.addTypes(resultTypes);
}
 
IncreasesOp IncreasesOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::TypeRange resultTypes, ::mlir::Value value) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(value)>(value));
  auto __res__ = ::llvm::dyn_cast<IncreasesOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
IncreasesOp IncreasesOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::TypeRange resultTypes, ::mlir::Value value) {
  return create(builder, builder.getLoc(), std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(value)>(value));
}
 
void IncreasesOp::build(::mlir::OpBuilder &, ::mlir::OperationState &odsState, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, ::llvm::ArrayRef<::mlir::NamedAttribute> attributes) {
  assert(operands.size() == 1u && "mismatched number of parameters");
  odsState.addOperands(operands);
  odsState.addAttributes(attributes);
  assert(resultTypes.size() == 0u && "mismatched number of return types");
  odsState.addTypes(resultTypes);
}
 
IncreasesOp IncreasesOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, ::llvm::ArrayRef<::mlir::NamedAttribute> attributes) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(operands)>(operands), std::forward<decltype(attributes)>(attributes));
  auto __res__ = ::llvm::dyn_cast<IncreasesOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
IncreasesOp IncreasesOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, ::llvm::ArrayRef<::mlir::NamedAttribute> attributes) {
  return create(builder, builder.getLoc(), std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(operands)>(operands), std::forward<decltype(attributes)>(attributes));
}
 
void IncreasesOp::build(::mlir::OpBuilder &, ::mlir::OperationState &odsState, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, const Properties &properties, ::llvm::ArrayRef<::mlir::NamedAttribute> discardableAttributes) {
  assert(operands.size() == 1u && "mismatched number of parameters");
  odsState.addOperands(operands);
  odsState.useProperties(const_cast<Properties&>(properties));
  odsState.addAttributes(discardableAttributes);
  assert(resultTypes.size() == 0u && "mismatched number of return types");
  odsState.addTypes(resultTypes);
}
 
IncreasesOp IncreasesOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, const Properties &properties, ::llvm::ArrayRef<::mlir::NamedAttribute> discardableAttributes) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(operands)>(operands), std::forward<decltype(properties)>(properties), std::forward<decltype(discardableAttributes)>(discardableAttributes));
  auto __res__ = ::llvm::dyn_cast<IncreasesOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
IncreasesOp IncreasesOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, const Properties &properties, ::llvm::ArrayRef<::mlir::NamedAttribute> discardableAttributes) {
  return create(builder, builder.getLoc(), std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(operands)>(operands), std::forward<decltype(properties)>(properties), std::forward<decltype(discardableAttributes)>(discardableAttributes));
}
 
::llvm::LogicalResult IncreasesOp::verifyInvariantsImpl() {
  {
    unsigned index = 0; (void)index;
    auto valueGroup0 = getODSOperands(0);
 
    for (auto v : valueGroup0) {
      if (::mlir::failed(__mlir_ods_local_type_constraint_Ops2(*this, v.getType(), "operand", index++)))
        return ::mlir::failure();
    }
  }
  return ::mlir::success();
}
 
::llvm::LogicalResult IncreasesOp::verifyInvariants() {
  return verifyInvariantsImpl();
}
 
::mlir::ParseResult IncreasesOp::parse(::mlir::OpAsmParser &parser, ::mlir::OperationState &result) {
  ::mlir::OpAsmParser::UnresolvedOperand valueRawOperand{};
  ::llvm::ArrayRef<::mlir::OpAsmParser::UnresolvedOperand> valueOperands(&valueRawOperand, 1);  ::llvm::SMLoc valueOperandsLoc;
  (void)valueOperandsLoc;
 
  valueOperandsLoc = parser.getCurrentLocation();
  if (parser.parseOperand(valueRawOperand))
    return ::mlir::failure();
  {
    auto loc = parser.getCurrentLocation();(void)loc;
    if (parser.parseOptionalAttrDict(result.attributes))
      return ::mlir::failure();
    if (failed(verifyInherentAttrs(result.name, result.attributes, [&]() {
        return parser.emitError(loc) << "'" << result.name.getStringRef() << "' op ";
      })))
      return ::mlir::failure();
  }
  ::mlir::Type odsBuildableType0 = ::llzk::felt::FeltType::get(parser.getBuilder().getContext());
  if (parser.resolveOperands(valueOperands, odsBuildableType0, valueOperandsLoc, result.operands))
    return ::mlir::failure();
  return ::mlir::success();
}
 
void IncreasesOp::print(::mlir::OpAsmPrinter &_odsPrinter) {
  _odsPrinter << ' ';
  _odsPrinter << getValue();
  ::llvm::SmallVector<::llvm::StringRef, 2> elidedAttrs;
  _odsPrinter.printOptionalAttrDict((*this)->getAttrs(), elidedAttrs);
}
 
// This side effect models "program termination". Based on
// https://github.com/llvm/llvm-project/blob/f325e4b2d836d6e65a4d0cf3efc6b0996ccf3765/mlir/lib/Dialect/ControlFlow/IR/ControlFlowOps.cpp#L92-L97
void IncreasesOp::getEffects(
    ::mlir::SmallVectorImpl<::mlir::SideEffects::EffectInstance<::mlir::MemoryEffects::Effect>> &effects
) {
  effects.emplace_back(::mlir::MemoryEffects::Write::get());
}
 
} // namespace llzk::verif
MLIR_DEFINE_EXPLICIT_TYPE_ID(::llzk::verif::IncreasesOp)
 
namespace llzk::verif {
 
 
//===----------------------------------------------------------------------===//
// ::llzk::verif::InvariantOp definitions
//===----------------------------------------------------------------------===//
 
namespace detail {
 
InvariantOpGenericAdaptorBase::InvariantOpGenericAdaptorBase(InvariantOp op) : odsAttrs(op->getRawDictionaryAttrs()), odsOpName(op->getName()), properties(op.getProperties()), odsRegions(op->getRegions()) {}
 
::llvm::StringRef InvariantOpGenericAdaptorBase::getLoopName() {
  auto attr = getLoopNameAttr();
  return attr.getValue();
}
 
::mlir::ArrayAttr InvariantOpGenericAdaptorBase::getLoopArgTypes() {
  auto attr = getLoopArgTypesAttr();
  return attr;
}
 
 
} // namespace detail
InvariantOpAdaptor::InvariantOpAdaptor(InvariantOp op) : InvariantOpGenericAdaptor(op->getOperands(), op) {}
 
::llvm::LogicalResult InvariantOpAdaptor::verify(::mlir::Location loc) {
  auto tblgen_loop_arg_types = getProperties().loop_arg_types; (void)tblgen_loop_arg_types;
  if (!tblgen_loop_arg_types) return emitError(loc, "'verif.invariant' op requires attribute 'loop_arg_types'");
  auto tblgen_loop_name = getProperties().loop_name; (void)tblgen_loop_name;
  if (!tblgen_loop_name) return emitError(loc, "'verif.invariant' op requires attribute 'loop_name'");
 
  if (tblgen_loop_name && !((::llvm::isa<::mlir::StringAttr>(tblgen_loop_name))))
    return emitError(loc, "'verif.invariant' op attribute 'loop_name' failed to satisfy constraint: string attribute");
 
  if (tblgen_loop_arg_types && !(((::llvm::isa<::mlir::ArrayAttr>(tblgen_loop_arg_types))) && (::llvm::all_of(::llvm::cast<::mlir::ArrayAttr>(tblgen_loop_arg_types), [&](::mlir::Attribute attr) { return attr && (((::llvm::isa<::mlir::TypeAttr>(attr))) && ((::llvm::isa<::mlir::Type>(::llvm::cast<::mlir::TypeAttr>(attr).getValue()))) && ((true))); }))))
    return emitError(loc, "'verif.invariant' op attribute 'loop_arg_types' failed to satisfy constraint: type array attribute");
  return ::mlir::success();
}
 
::llvm::LogicalResult InvariantOp::setPropertiesFromAttr(Properties &prop, ::mlir::Attribute attr, ::llvm::function_ref<::mlir::InFlightDiagnostic()> emitError) {
  ::mlir::DictionaryAttr dict = ::llvm::dyn_cast<::mlir::DictionaryAttr>(attr);
  if (!dict) {
    emitError() << "expected DictionaryAttr to set properties";
    return ::mlir::failure();
  }
 
  {
    auto &propStorage = prop.loop_arg_types;
       auto attr = dict.get("loop_arg_types");
    if (attr) {
      auto convertedAttr = ::llvm::dyn_cast<std::remove_reference_t<decltype(propStorage)>>(attr);
      if (convertedAttr) {
        propStorage = convertedAttr;
      } else {
        emitError() << "Invalid attribute `loop_arg_types` in property conversion: " << attr;
        return ::mlir::failure();
      }
    }
  }
 
  {
    auto &propStorage = prop.loop_name;
       auto attr = dict.get("loop_name");
    if (attr) {
      auto convertedAttr = ::llvm::dyn_cast<std::remove_reference_t<decltype(propStorage)>>(attr);
      if (convertedAttr) {
        propStorage = convertedAttr;
      } else {
        emitError() << "Invalid attribute `loop_name` in property conversion: " << attr;
        return ::mlir::failure();
      }
    }
  }
  return ::mlir::success();
}
 
::mlir::Attribute InvariantOp::getPropertiesAsAttr(::mlir::MLIRContext *ctx, const Properties &prop) {
    ::mlir::SmallVector<::mlir::NamedAttribute> attrs;
    ::mlir::Builder odsBuilder{ctx};
 
    {
      const auto &propStorage = prop.loop_arg_types;
      if (propStorage)
        attrs.push_back(odsBuilder.getNamedAttr("loop_arg_types",
                                       propStorage));
    }
 
    {
      const auto &propStorage = prop.loop_name;
      if (propStorage)
        attrs.push_back(odsBuilder.getNamedAttr("loop_name",
                                       propStorage));
    }
 
  if (!attrs.empty())
    return odsBuilder.getDictionaryAttr(attrs);
  return {};
}
 
llvm::hash_code InvariantOp::computePropertiesHash(const Properties &prop) {
  using llvm::hash_value;
  return llvm::hash_combine(
    llvm::hash_value(prop.loop_arg_types.getAsOpaquePointer()), 
    llvm::hash_value(prop.loop_name.getAsOpaquePointer()));
}
 
std::optional<mlir::Attribute> InvariantOp::getInherentAttr(::mlir::MLIRContext *ctx, const Properties &prop, llvm::StringRef name) {
    if (name == "loop_arg_types")
      return prop.loop_arg_types;
 
    if (name == "loop_name")
      return prop.loop_name;
  return std::nullopt;
}
 
void InvariantOp::setInherentAttr(Properties &prop, llvm::StringRef name, mlir::Attribute value) {
    if (name == "loop_arg_types") {
       prop.loop_arg_types = ::llvm::dyn_cast_or_null<std::remove_reference_t<decltype(prop.loop_arg_types)>>(value);
       return;
    }
 
    if (name == "loop_name") {
       prop.loop_name = ::llvm::dyn_cast_or_null<std::remove_reference_t<decltype(prop.loop_name)>>(value);
       return;
    }
}
 
void InvariantOp::populateInherentAttrs(::mlir::MLIRContext *ctx, const Properties &prop, ::mlir::NamedAttrList &attrs) {
    if (prop.loop_arg_types) attrs.append("loop_arg_types", prop.loop_arg_types);
 
    if (prop.loop_name) attrs.append("loop_name", prop.loop_name);
}
 
::llvm::LogicalResult InvariantOp::verifyInherentAttrs(::mlir::OperationName opName, ::mlir::NamedAttrList &attrs, llvm::function_ref<::mlir::InFlightDiagnostic()> emitError) {
    {
      ::mlir::Attribute attr = attrs.get(getLoopArgTypesAttrName(opName));
      if (attr && ::mlir::failed(__mlir_ods_local_attr_constraint_Ops7(attr, "loop_arg_types", emitError)))
        return ::mlir::failure();
    }
 
    {
      ::mlir::Attribute attr = attrs.get(getLoopNameAttrName(opName));
      if (attr && ::mlir::failed(__mlir_ods_local_attr_constraint_Ops1(attr, "loop_name", emitError)))
        return ::mlir::failure();
    }
    return ::mlir::success();
}
 
::llvm::LogicalResult InvariantOp::readProperties(::mlir::DialectBytecodeReader &reader, ::mlir::OperationState &state) {
  auto &prop = state.getOrAddProperties<Properties>(); (void)prop;
  if (::mlir::failed(reader.readAttribute(prop.loop_arg_types)))
    return ::mlir::failure();
 
  if (::mlir::failed(reader.readAttribute(prop.loop_name)))
    return ::mlir::failure();
  return ::mlir::success();
}
 
void InvariantOp::writeProperties(::mlir::DialectBytecodeWriter &writer) {
  auto &prop = getProperties(); (void)prop;
  writer.writeAttribute(prop.loop_arg_types);
  writer.writeAttribute(prop.loop_name);
}
 
::llvm::StringRef InvariantOp::getLoopName() {
  auto attr = getLoopNameAttr();
  return attr.getValue();
}
 
::mlir::ArrayAttr InvariantOp::getLoopArgTypes() {
  auto attr = getLoopArgTypesAttr();
  return attr;
}
 
void InvariantOp::setLoopName(::llvm::StringRef attrValue) {
  getProperties().loop_name = ::mlir::Builder((*this)->getContext()).getStringAttr(attrValue);
}
 
InvariantOp InvariantOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::StringRef loop_name, ::llvm::ArrayRef<::mlir::Type> loop_arg_types, ::llvm::ArrayRef<::mlir::Location> loop_arg_locs) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(loop_name)>(loop_name), std::forward<decltype(loop_arg_types)>(loop_arg_types), std::forward<decltype(loop_arg_locs)>(loop_arg_locs));
  auto __res__ = ::llvm::dyn_cast<InvariantOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
InvariantOp InvariantOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::StringRef loop_name, ::llvm::ArrayRef<::mlir::Type> loop_arg_types, ::llvm::ArrayRef<::mlir::Location> loop_arg_locs) {
  return create(builder, builder.getLoc(), std::forward<decltype(loop_name)>(loop_name), std::forward<decltype(loop_arg_types)>(loop_arg_types), std::forward<decltype(loop_arg_locs)>(loop_arg_locs));
}
 
::llvm::LogicalResult InvariantOp::verifyInvariantsImpl() {
  auto tblgen_loop_arg_types = getProperties().loop_arg_types; (void)tblgen_loop_arg_types;
  if (!tblgen_loop_arg_types) return emitOpError("requires attribute 'loop_arg_types'");
  auto tblgen_loop_name = getProperties().loop_name; (void)tblgen_loop_name;
  if (!tblgen_loop_name) return emitOpError("requires attribute 'loop_name'");
 
  if (::mlir::failed(__mlir_ods_local_attr_constraint_Ops1(*this, tblgen_loop_name, "loop_name")))
    return ::mlir::failure();
 
  if (::mlir::failed(__mlir_ods_local_attr_constraint_Ops7(*this, tblgen_loop_arg_types, "loop_arg_types")))
    return ::mlir::failure();
  {
    unsigned index = 0; (void)index;
 
    for (auto &region : ::llvm::MutableArrayRef((*this)->getRegion(0)))
      if (::mlir::failed(__mlir_ods_local_region_constraint_Ops2(*this, region, "region", index++)))
        return ::mlir::failure();
  }
  return ::mlir::success();
}
 
::llvm::LogicalResult InvariantOp::verifyInvariants() {
  if(::mlir::succeeded(verifyInvariantsImpl()) && ::mlir::succeeded(verify()))
    return ::mlir::success();
  return ::mlir::failure();
}
 
::llvm::LogicalResult InvariantOp::setPropertiesFromParsedAttr(Properties &prop, ::mlir::Attribute attr, ::llvm::function_ref<::mlir::InFlightDiagnostic()> emitError) {
  ::mlir::DictionaryAttr dict = ::llvm::dyn_cast<::mlir::DictionaryAttr>(attr);
  if (!dict) {
    emitError() << "expected DictionaryAttr to set properties";
    return ::mlir::failure();
  }
  // keep track of used keys in the input dictionary to be able to error out
  // if there are some unknown ones.
  ::mlir::DenseSet<::mlir::StringAttr> usedKeys;
  ::mlir::MLIRContext *ctx = dict.getContext();
  (void)ctx;
  {
 
    auto &propStorage = prop.loop_name;
    auto loop_nameAttrName = ::mlir::StringAttr::get(ctx, "loop_name");
    auto attr = dict.get(loop_nameAttrName);
    usedKeys.insert(loop_nameAttrName);
    if (attr || /*isRequired=*/true) {
      if (!attr) {
        emitError() << "expected key entry for loop_name in DictionaryAttr to set "
                   "Properties.";
        return ::mlir::failure();
      }
      auto convertedAttr = ::llvm::dyn_cast<std::remove_reference_t<decltype(propStorage)>>(attr);
      if (convertedAttr) {
        propStorage = convertedAttr;
      } else {
        emitError() << "Invalid attribute `loop_name` in property conversion: " << attr;
        return ::mlir::failure();
      }
    }
  }
  {
 
    auto &propStorage = prop.loop_arg_types;
    auto loop_arg_typesAttrName = ::mlir::StringAttr::get(ctx, "loop_arg_types");
    auto attr = dict.get(loop_arg_typesAttrName);
    usedKeys.insert(loop_arg_typesAttrName);
    if (attr || /*isRequired=*/true) {
      if (!attr) {
        emitError() << "expected key entry for loop_arg_types in DictionaryAttr to set "
                   "Properties.";
        return ::mlir::failure();
      }
      auto convertedAttr = ::llvm::dyn_cast<std::remove_reference_t<decltype(propStorage)>>(attr);
      if (convertedAttr) {
        propStorage = convertedAttr;
      } else {
        emitError() << "Invalid attribute `loop_arg_types` in property conversion: " << attr;
        return ::mlir::failure();
      }
    }
  }
 
  for (::mlir::NamedAttribute attr : dict) {
    if (!usedKeys.contains(attr.getName()))
      return emitError() << "unknown key '" << attr.getName() <<
          "' when parsing properties dictionary";
  }
  return ::mlir::success();
}
 
 
} // namespace llzk::verif
MLIR_DEFINE_EXPLICIT_TYPE_ID(::llzk::verif::InvariantOp)
MLIR_DEFINE_EXPLICIT_TYPE_ID(::llzk::verif::detail::InvariantOpGenericAdaptorBase::Properties)
 
namespace llzk::verif {
 
 
//===----------------------------------------------------------------------===//
// ::llzk::verif::OldOp definitions
//===----------------------------------------------------------------------===//
 
namespace detail {
 
OldOpGenericAdaptorBase::OldOpGenericAdaptorBase(OldOp op) : odsAttrs(op->getRawDictionaryAttrs()), odsOpName(op->getName()), properties(op.getProperties()), odsRegions(op->getRegions()) {}
 
 
} // namespace detail
OldOpAdaptor::OldOpAdaptor(OldOp op) : OldOpGenericAdaptor(op->getOperands(), op) {}
 
::llvm::LogicalResult OldOpAdaptor::verify(::mlir::Location loc) {
  return ::mlir::success();
}
 
::llvm::LogicalResult OldOp::setPropertiesFromAttr(Properties &prop, ::mlir::Attribute attr, ::llvm::function_ref<::mlir::InFlightDiagnostic()> emitError) {
  ::mlir::DictionaryAttr dict = ::llvm::dyn_cast<::mlir::DictionaryAttr>(attr);
  if (!dict) {
    emitError() << "expected DictionaryAttr to set properties";
    return ::mlir::failure();
  }
      return ::mlir::success();
}
 
::mlir::Attribute OldOp::getPropertiesAsAttr(::mlir::MLIRContext *ctx, const Properties &prop) {
    ::mlir::SmallVector<::mlir::NamedAttribute> attrs;
    ::mlir::Builder odsBuilder{ctx};
 
  if (!attrs.empty())
    return odsBuilder.getDictionaryAttr(attrs);
  return {};
}
 
llvm::hash_code OldOp::computePropertiesHash(const Properties &prop) {
  using llvm::hash_value;
  return llvm::hash_combine();
}
 
std::optional<mlir::Attribute> OldOp::getInherentAttr(::mlir::MLIRContext *ctx, const Properties &prop, llvm::StringRef name) {
  return std::nullopt;
}
 
void OldOp::setInherentAttr(Properties &prop, llvm::StringRef name, mlir::Attribute value) {
}
 
void OldOp::populateInherentAttrs(::mlir::MLIRContext *ctx, const Properties &prop, ::mlir::NamedAttrList &attrs) {
}
 
::llvm::LogicalResult OldOp::verifyInherentAttrs(::mlir::OperationName opName, ::mlir::NamedAttrList &attrs, llvm::function_ref<::mlir::InFlightDiagnostic()> emitError) {
    return ::mlir::success();
}
 
void OldOp::build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, ::mlir::Type result, ::mlir::Value value) {
  odsState.addOperands(value);
  odsState.addTypes(result);
}
 
OldOp OldOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::Type result, ::mlir::Value value) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(result)>(result), std::forward<decltype(value)>(value));
  auto __res__ = ::llvm::dyn_cast<OldOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
OldOp OldOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::Type result, ::mlir::Value value) {
  return create(builder, builder.getLoc(), std::forward<decltype(result)>(result), std::forward<decltype(value)>(value));
}
 
void OldOp::build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, ::mlir::Value value) {
  odsState.addOperands(value);
 
        ::llvm::SmallVector<::mlir::Type, 2> inferredReturnTypes;
        if (::mlir::succeeded(OldOp::inferReturnTypes(odsBuilder.getContext(),
                      odsState.location, odsState.operands,
                      odsState.attributes.getDictionary(odsState.getContext()),
                      odsState.getRawProperties(),
                      odsState.regions, inferredReturnTypes)))
          odsState.addTypes(inferredReturnTypes);
        else
          ::mlir::detail::reportFatalInferReturnTypesError(odsState);
        
}
 
OldOp OldOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::Value value) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(value)>(value));
  auto __res__ = ::llvm::dyn_cast<OldOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
OldOp OldOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::Value value) {
  return create(builder, builder.getLoc(), std::forward<decltype(value)>(value));
}
 
void OldOp::build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, ::mlir::TypeRange resultTypes, ::mlir::Value value) {
  odsState.addOperands(value);
  assert(resultTypes.size() == 1u && "mismatched number of results");
  odsState.addTypes(resultTypes);
}
 
OldOp OldOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::TypeRange resultTypes, ::mlir::Value value) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(value)>(value));
  auto __res__ = ::llvm::dyn_cast<OldOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
OldOp OldOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::TypeRange resultTypes, ::mlir::Value value) {
  return create(builder, builder.getLoc(), std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(value)>(value));
}
 
void OldOp::build(::mlir::OpBuilder &, ::mlir::OperationState &odsState, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, ::llvm::ArrayRef<::mlir::NamedAttribute> attributes) {
  assert(operands.size() == 1u && "mismatched number of parameters");
  odsState.addOperands(operands);
  odsState.addAttributes(attributes);
  assert(resultTypes.size() == 1u && "mismatched number of return types");
  odsState.addTypes(resultTypes);
}
 
OldOp OldOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, ::llvm::ArrayRef<::mlir::NamedAttribute> attributes) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(operands)>(operands), std::forward<decltype(attributes)>(attributes));
  auto __res__ = ::llvm::dyn_cast<OldOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
OldOp OldOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, ::llvm::ArrayRef<::mlir::NamedAttribute> attributes) {
  return create(builder, builder.getLoc(), std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(operands)>(operands), std::forward<decltype(attributes)>(attributes));
}
 
void OldOp::build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, ::mlir::ValueRange operands, ::llvm::ArrayRef<::mlir::NamedAttribute> attributes) {
  assert(operands.size() == 1u && "mismatched number of parameters");
  odsState.addOperands(operands);
  odsState.addAttributes(attributes);
 
  ::llvm::SmallVector<::mlir::Type, 2> inferredReturnTypes;
  if (::mlir::succeeded(OldOp::inferReturnTypes(odsBuilder.getContext(),
          odsState.location, operands,
          odsState.attributes.getDictionary(odsState.getContext()),
          odsState.getRawProperties(),
          odsState.regions, inferredReturnTypes))) {
    assert(inferredReturnTypes.size() == 1u && "mismatched number of return types");
    odsState.addTypes(inferredReturnTypes);
  } else {
    ::llvm::report_fatal_error("Failed to infer result type(s).");
  }
}
 
OldOp OldOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::ValueRange operands, ::llvm::ArrayRef<::mlir::NamedAttribute> attributes) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(operands)>(operands), std::forward<decltype(attributes)>(attributes));
  auto __res__ = ::llvm::dyn_cast<OldOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
OldOp OldOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::ValueRange operands, ::llvm::ArrayRef<::mlir::NamedAttribute> attributes) {
  return create(builder, builder.getLoc(), std::forward<decltype(operands)>(operands), std::forward<decltype(attributes)>(attributes));
}
 
void OldOp::build(::mlir::OpBuilder &, ::mlir::OperationState &odsState, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, const Properties &properties, ::llvm::ArrayRef<::mlir::NamedAttribute> discardableAttributes) {
  assert(operands.size() == 1u && "mismatched number of parameters");
  odsState.addOperands(operands);
  odsState.useProperties(const_cast<Properties&>(properties));
  odsState.addAttributes(discardableAttributes);
  assert(resultTypes.size() == 1u && "mismatched number of return types");
  odsState.addTypes(resultTypes);
}
 
OldOp OldOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, const Properties &properties, ::llvm::ArrayRef<::mlir::NamedAttribute> discardableAttributes) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(operands)>(operands), std::forward<decltype(properties)>(properties), std::forward<decltype(discardableAttributes)>(discardableAttributes));
  auto __res__ = ::llvm::dyn_cast<OldOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
OldOp OldOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, const Properties &properties, ::llvm::ArrayRef<::mlir::NamedAttribute> discardableAttributes) {
  return create(builder, builder.getLoc(), std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(operands)>(operands), std::forward<decltype(properties)>(properties), std::forward<decltype(discardableAttributes)>(discardableAttributes));
}
 
void OldOp::build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, ::mlir::ValueRange operands, const Properties &properties, ::llvm::ArrayRef<::mlir::NamedAttribute> discardableAttributes) {
  assert(operands.size() == 1u && "mismatched number of parameters");
  odsState.addOperands(operands);
  odsState.useProperties(const_cast<Properties &>(properties));
  odsState.addAttributes(discardableAttributes);
 
  ::llvm::SmallVector<::mlir::Type, 2> inferredReturnTypes;
  if (::mlir::succeeded(OldOp::inferReturnTypes(odsBuilder.getContext(),
          odsState.location, operands,
          odsState.attributes.getDictionary(odsState.getContext()),
          odsState.getRawProperties(),
          odsState.regions, inferredReturnTypes))) {
    assert(inferredReturnTypes.size() == 1u && "mismatched number of return types");
    odsState.addTypes(inferredReturnTypes);
  } else {
    ::llvm::report_fatal_error("Failed to infer result type(s).");
  }
}
 
OldOp OldOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::ValueRange operands, const Properties &properties, ::llvm::ArrayRef<::mlir::NamedAttribute> discardableAttributes) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(operands)>(operands), std::forward<decltype(properties)>(properties), std::forward<decltype(discardableAttributes)>(discardableAttributes));
  auto __res__ = ::llvm::dyn_cast<OldOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
OldOp OldOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::ValueRange operands, const Properties &properties, ::llvm::ArrayRef<::mlir::NamedAttribute> discardableAttributes) {
  return create(builder, builder.getLoc(), std::forward<decltype(operands)>(operands), std::forward<decltype(properties)>(properties), std::forward<decltype(discardableAttributes)>(discardableAttributes));
}
 
::llvm::LogicalResult OldOp::verifyInvariantsImpl() {
  {
    unsigned index = 0; (void)index;
    auto valueGroup0 = getODSOperands(0);
 
    for (auto v : valueGroup0) {
      if (::mlir::failed(__mlir_ods_local_type_constraint_Ops6(*this, v.getType(), "operand", index++)))
        return ::mlir::failure();
    }
  }
  {
    unsigned index = 0; (void)index;
    auto valueGroup0 = getODSResults(0);
 
    for (auto v : valueGroup0) {
      if (::mlir::failed(__mlir_ods_local_type_constraint_Ops6(*this, v.getType(), "result", index++)))
        return ::mlir::failure();
    }
  }
  if (!((((*this->getODSOperands(0).begin()).getType()) == ((*this->getODSResults(0).begin()).getType()) && ((*this->getODSResults(0).begin()).getType()) == ((*this->getODSOperands(0).begin()).getType()))))
    return emitOpError("failed to verify that all of {value, result} have same type");
  return ::mlir::success();
}
 
::llvm::LogicalResult OldOp::verifyInvariants() {
  return verifyInvariantsImpl();
}
 
::llvm::LogicalResult OldOp::inferReturnTypes(::mlir::MLIRContext *context, ::std::optional<::mlir::Location> location, ::mlir::ValueRange operands, ::mlir::DictionaryAttr attributes, ::mlir::PropertyRef properties, ::mlir::RegionRange regions, ::llvm::SmallVectorImpl<::mlir::Type>&inferredReturnTypes) {
  inferredReturnTypes.resize(1);
  ::mlir::Builder odsBuilder(context);
  if (operands.size() <= 0)
    return ::mlir::failure();
  ::mlir::Type odsInferredType0 = operands[0].getType();
  inferredReturnTypes[0] = odsInferredType0;
  return ::mlir::success();
}
 
::mlir::ParseResult OldOp::parse(::mlir::OpAsmParser &parser, ::mlir::OperationState &result) {
  ::mlir::OpAsmParser::UnresolvedOperand valueRawOperand{};
  ::llvm::ArrayRef<::mlir::OpAsmParser::UnresolvedOperand> valueOperands(&valueRawOperand, 1);  ::llvm::SMLoc valueOperandsLoc;
  (void)valueOperandsLoc;
  ::mlir::Type resultRawType{};
  ::llvm::ArrayRef<::mlir::Type> resultTypes(&resultRawType, 1);
 
  valueOperandsLoc = parser.getCurrentLocation();
  if (parser.parseOperand(valueRawOperand))
    return ::mlir::failure();
  if (parser.parseColon())
    return ::mlir::failure();
 
  {
    ::mlir::Type type;
    if (parser.parseCustomTypeWithFallback(type))
      return ::mlir::failure();
    resultRawType = type;
  }
  {
    auto loc = parser.getCurrentLocation();(void)loc;
    if (parser.parseOptionalAttrDict(result.attributes))
      return ::mlir::failure();
    if (failed(verifyInherentAttrs(result.name, result.attributes, [&]() {
        return parser.emitError(loc) << "'" << result.name.getStringRef() << "' op ";
      })))
      return ::mlir::failure();
  }
  result.addTypes(resultTypes);
  if (parser.resolveOperands(valueOperands, resultTypes[0], valueOperandsLoc, result.operands))
    return ::mlir::failure();
  return ::mlir::success();
}
 
void OldOp::print(::mlir::OpAsmPrinter &_odsPrinter) {
  _odsPrinter << ' ';
  _odsPrinter << getValue();
  _odsPrinter << ' ' << ":";
  _odsPrinter << ' ';
  {
    auto type = getResult().getType();
    if (auto validType = ::llvm::dyn_cast<::mlir::Type>(type))
      _odsPrinter.printStrippedAttrOrType(validType);
   else
     _odsPrinter << type;
  }
  ::llvm::SmallVector<::llvm::StringRef, 2> elidedAttrs;
  _odsPrinter.printOptionalAttrDict((*this)->getAttrs(), elidedAttrs);
}
 
void OldOp::getEffects(::llvm::SmallVectorImpl<::mlir::SideEffects::EffectInstance<::mlir::MemoryEffects::Effect>> &effects) {
}
 
 
} // namespace llzk::verif
MLIR_DEFINE_EXPLICIT_TYPE_ID(::llzk::verif::OldOp)
 
namespace llzk::verif {
 
 
//===----------------------------------------------------------------------===//
// ::llzk::verif::ProveDetOp definitions
//===----------------------------------------------------------------------===//
 
namespace detail {
 
ProveDetOpGenericAdaptorBase::ProveDetOpGenericAdaptorBase(ProveDetOp op) : odsAttrs(op->getRawDictionaryAttrs()), odsOpName(op->getName()), properties(op.getProperties()), odsRegions(op->getRegions()) {}
 
 
} // namespace detail
ProveDetOpAdaptor::ProveDetOpAdaptor(ProveDetOp op) : ProveDetOpGenericAdaptor(op->getOperands(), op) {}
 
::llvm::LogicalResult ProveDetOpAdaptor::verify(::mlir::Location loc) {
  return ::mlir::success();
}
 
::llvm::LogicalResult ProveDetOp::setPropertiesFromAttr(Properties &prop, ::mlir::Attribute attr, ::llvm::function_ref<::mlir::InFlightDiagnostic()> emitError) {
  ::mlir::DictionaryAttr dict = ::llvm::dyn_cast<::mlir::DictionaryAttr>(attr);
  if (!dict) {
    emitError() << "expected DictionaryAttr to set properties";
    return ::mlir::failure();
  }
      return ::mlir::success();
}
 
::mlir::Attribute ProveDetOp::getPropertiesAsAttr(::mlir::MLIRContext *ctx, const Properties &prop) {
    ::mlir::SmallVector<::mlir::NamedAttribute> attrs;
    ::mlir::Builder odsBuilder{ctx};
 
  if (!attrs.empty())
    return odsBuilder.getDictionaryAttr(attrs);
  return {};
}
 
llvm::hash_code ProveDetOp::computePropertiesHash(const Properties &prop) {
  using llvm::hash_value;
  return llvm::hash_combine();
}
 
std::optional<mlir::Attribute> ProveDetOp::getInherentAttr(::mlir::MLIRContext *ctx, const Properties &prop, llvm::StringRef name) {
  return std::nullopt;
}
 
void ProveDetOp::setInherentAttr(Properties &prop, llvm::StringRef name, mlir::Attribute value) {
}
 
void ProveDetOp::populateInherentAttrs(::mlir::MLIRContext *ctx, const Properties &prop, ::mlir::NamedAttrList &attrs) {
}
 
::llvm::LogicalResult ProveDetOp::verifyInherentAttrs(::mlir::OperationName opName, ::mlir::NamedAttrList &attrs, llvm::function_ref<::mlir::InFlightDiagnostic()> emitError) {
    return ::mlir::success();
}
 
void ProveDetOp::build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, ::mlir::Type result, ::mlir::Value condition) {
  odsState.addOperands(condition);
  odsState.addTypes(result);
}
 
ProveDetOp ProveDetOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::Type result, ::mlir::Value condition) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(result)>(result), std::forward<decltype(condition)>(condition));
  auto __res__ = ::llvm::dyn_cast<ProveDetOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
ProveDetOp ProveDetOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::Type result, ::mlir::Value condition) {
  return create(builder, builder.getLoc(), std::forward<decltype(result)>(result), std::forward<decltype(condition)>(condition));
}
 
void ProveDetOp::build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, ::mlir::Value condition) {
  odsState.addOperands(condition);
 
        ::llvm::SmallVector<::mlir::Type, 2> inferredReturnTypes;
        if (::mlir::succeeded(ProveDetOp::inferReturnTypes(odsBuilder.getContext(),
                      odsState.location, odsState.operands,
                      odsState.attributes.getDictionary(odsState.getContext()),
                      odsState.getRawProperties(),
                      odsState.regions, inferredReturnTypes)))
          odsState.addTypes(inferredReturnTypes);
        else
          ::mlir::detail::reportFatalInferReturnTypesError(odsState);
        
}
 
ProveDetOp ProveDetOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::Value condition) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(condition)>(condition));
  auto __res__ = ::llvm::dyn_cast<ProveDetOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
ProveDetOp ProveDetOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::Value condition) {
  return create(builder, builder.getLoc(), std::forward<decltype(condition)>(condition));
}
 
void ProveDetOp::build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, ::mlir::TypeRange resultTypes, ::mlir::Value condition) {
  odsState.addOperands(condition);
  assert(resultTypes.size() == 1u && "mismatched number of results");
  odsState.addTypes(resultTypes);
}
 
ProveDetOp ProveDetOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::TypeRange resultTypes, ::mlir::Value condition) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(condition)>(condition));
  auto __res__ = ::llvm::dyn_cast<ProveDetOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
ProveDetOp ProveDetOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::TypeRange resultTypes, ::mlir::Value condition) {
  return create(builder, builder.getLoc(), std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(condition)>(condition));
}
 
void ProveDetOp::build(::mlir::OpBuilder &, ::mlir::OperationState &odsState, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, ::llvm::ArrayRef<::mlir::NamedAttribute> attributes) {
  assert(operands.size() == 1u && "mismatched number of parameters");
  odsState.addOperands(operands);
  odsState.addAttributes(attributes);
  assert(resultTypes.size() == 1u && "mismatched number of return types");
  odsState.addTypes(resultTypes);
}
 
ProveDetOp ProveDetOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, ::llvm::ArrayRef<::mlir::NamedAttribute> attributes) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(operands)>(operands), std::forward<decltype(attributes)>(attributes));
  auto __res__ = ::llvm::dyn_cast<ProveDetOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
ProveDetOp ProveDetOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, ::llvm::ArrayRef<::mlir::NamedAttribute> attributes) {
  return create(builder, builder.getLoc(), std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(operands)>(operands), std::forward<decltype(attributes)>(attributes));
}
 
void ProveDetOp::build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, ::mlir::ValueRange operands, ::llvm::ArrayRef<::mlir::NamedAttribute> attributes) {
  assert(operands.size() == 1u && "mismatched number of parameters");
  odsState.addOperands(operands);
  odsState.addAttributes(attributes);
 
  ::llvm::SmallVector<::mlir::Type, 2> inferredReturnTypes;
  if (::mlir::succeeded(ProveDetOp::inferReturnTypes(odsBuilder.getContext(),
          odsState.location, operands,
          odsState.attributes.getDictionary(odsState.getContext()),
          odsState.getRawProperties(),
          odsState.regions, inferredReturnTypes))) {
    assert(inferredReturnTypes.size() == 1u && "mismatched number of return types");
    odsState.addTypes(inferredReturnTypes);
  } else {
    ::llvm::report_fatal_error("Failed to infer result type(s).");
  }
}
 
ProveDetOp ProveDetOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::ValueRange operands, ::llvm::ArrayRef<::mlir::NamedAttribute> attributes) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(operands)>(operands), std::forward<decltype(attributes)>(attributes));
  auto __res__ = ::llvm::dyn_cast<ProveDetOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
ProveDetOp ProveDetOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::ValueRange operands, ::llvm::ArrayRef<::mlir::NamedAttribute> attributes) {
  return create(builder, builder.getLoc(), std::forward<decltype(operands)>(operands), std::forward<decltype(attributes)>(attributes));
}
 
void ProveDetOp::build(::mlir::OpBuilder &, ::mlir::OperationState &odsState, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, const Properties &properties, ::llvm::ArrayRef<::mlir::NamedAttribute> discardableAttributes) {
  assert(operands.size() == 1u && "mismatched number of parameters");
  odsState.addOperands(operands);
  odsState.useProperties(const_cast<Properties&>(properties));
  odsState.addAttributes(discardableAttributes);
  assert(resultTypes.size() == 1u && "mismatched number of return types");
  odsState.addTypes(resultTypes);
}
 
ProveDetOp ProveDetOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, const Properties &properties, ::llvm::ArrayRef<::mlir::NamedAttribute> discardableAttributes) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(operands)>(operands), std::forward<decltype(properties)>(properties), std::forward<decltype(discardableAttributes)>(discardableAttributes));
  auto __res__ = ::llvm::dyn_cast<ProveDetOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
ProveDetOp ProveDetOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, const Properties &properties, ::llvm::ArrayRef<::mlir::NamedAttribute> discardableAttributes) {
  return create(builder, builder.getLoc(), std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(operands)>(operands), std::forward<decltype(properties)>(properties), std::forward<decltype(discardableAttributes)>(discardableAttributes));
}
 
void ProveDetOp::build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, ::mlir::ValueRange operands, const Properties &properties, ::llvm::ArrayRef<::mlir::NamedAttribute> discardableAttributes) {
  assert(operands.size() == 1u && "mismatched number of parameters");
  odsState.addOperands(operands);
  odsState.useProperties(const_cast<Properties &>(properties));
  odsState.addAttributes(discardableAttributes);
 
  ::llvm::SmallVector<::mlir::Type, 2> inferredReturnTypes;
  if (::mlir::succeeded(ProveDetOp::inferReturnTypes(odsBuilder.getContext(),
          odsState.location, operands,
          odsState.attributes.getDictionary(odsState.getContext()),
          odsState.getRawProperties(),
          odsState.regions, inferredReturnTypes))) {
    assert(inferredReturnTypes.size() == 1u && "mismatched number of return types");
    odsState.addTypes(inferredReturnTypes);
  } else {
    ::llvm::report_fatal_error("Failed to infer result type(s).");
  }
}
 
ProveDetOp ProveDetOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::ValueRange operands, const Properties &properties, ::llvm::ArrayRef<::mlir::NamedAttribute> discardableAttributes) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(operands)>(operands), std::forward<decltype(properties)>(properties), std::forward<decltype(discardableAttributes)>(discardableAttributes));
  auto __res__ = ::llvm::dyn_cast<ProveDetOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
ProveDetOp ProveDetOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::ValueRange operands, const Properties &properties, ::llvm::ArrayRef<::mlir::NamedAttribute> discardableAttributes) {
  return create(builder, builder.getLoc(), std::forward<decltype(operands)>(operands), std::forward<decltype(properties)>(properties), std::forward<decltype(discardableAttributes)>(discardableAttributes));
}
 
::llvm::LogicalResult ProveDetOp::verifyInvariantsImpl() {
  {
    unsigned index = 0; (void)index;
    auto valueGroup0 = getODSOperands(0);
 
    for (auto v : valueGroup0) {
      if (::mlir::failed(__mlir_ods_local_type_constraint_Ops1(*this, v.getType(), "operand", index++)))
        return ::mlir::failure();
    }
  }
  {
    unsigned index = 0; (void)index;
    auto valueGroup0 = getODSResults(0);
 
    for (auto v : valueGroup0) {
      if (::mlir::failed(__mlir_ods_local_type_constraint_Ops3(*this, v.getType(), "result", index++)))
        return ::mlir::failure();
    }
  }
  return ::mlir::success();
}
 
::llvm::LogicalResult ProveDetOp::verifyInvariants() {
  return verifyInvariantsImpl();
}
 
::llvm::LogicalResult ProveDetOp::inferReturnTypes(::mlir::MLIRContext *context, ::std::optional<::mlir::Location> location, ::mlir::ValueRange operands, ::mlir::DictionaryAttr attributes, ::mlir::PropertyRef properties, ::mlir::RegionRange regions, ::llvm::SmallVectorImpl<::mlir::Type>&inferredReturnTypes) {
  inferredReturnTypes.resize(1);
  ::mlir::Builder odsBuilder(context);
  ::mlir::Type odsInferredType0 = odsBuilder.getIntegerType(1);
  inferredReturnTypes[0] = odsInferredType0;
  return ::mlir::success();
}
 
::mlir::ParseResult ProveDetOp::parse(::mlir::OpAsmParser &parser, ::mlir::OperationState &result) {
  ::mlir::OpAsmParser::UnresolvedOperand conditionRawOperand{};
  ::llvm::ArrayRef<::mlir::OpAsmParser::UnresolvedOperand> conditionOperands(&conditionRawOperand, 1);  ::llvm::SMLoc conditionOperandsLoc;
  (void)conditionOperandsLoc;
  ::mlir::Type conditionRawType{};
  ::llvm::ArrayRef<::mlir::Type> conditionTypes(&conditionRawType, 1);
 
  conditionOperandsLoc = parser.getCurrentLocation();
  if (parser.parseOperand(conditionRawOperand))
    return ::mlir::failure();
  {
    auto loc = parser.getCurrentLocation();(void)loc;
    if (parser.parseOptionalAttrDict(result.attributes))
      return ::mlir::failure();
    if (failed(verifyInherentAttrs(result.name, result.attributes, [&]() {
        return parser.emitError(loc) << "'" << result.name.getStringRef() << "' op ";
      })))
      return ::mlir::failure();
  }
  if (parser.parseColon())
    return ::mlir::failure();
 
  {
    ::mlir::Type type;
    if (parser.parseCustomTypeWithFallback(type))
      return ::mlir::failure();
    conditionRawType = type;
  }
  ::mlir::Type odsBuildableType0 = parser.getBuilder().getIntegerType(1);
  result.addTypes(odsBuildableType0);
  if (parser.resolveOperands(conditionOperands, conditionTypes, conditionOperandsLoc, result.operands))
    return ::mlir::failure();
  return ::mlir::success();
}
 
void ProveDetOp::print(::mlir::OpAsmPrinter &_odsPrinter) {
  _odsPrinter << ' ';
  _odsPrinter << getCondition();
  ::llvm::SmallVector<::llvm::StringRef, 2> elidedAttrs;
  _odsPrinter.printOptionalAttrDict((*this)->getAttrs(), elidedAttrs);
  _odsPrinter << ' ' << ":";
  _odsPrinter << ' ';
  {
    auto type = getCondition().getType();
    if (auto validType = ::llvm::dyn_cast<::mlir::Type>(type))
      _odsPrinter.printStrippedAttrOrType(validType);
   else
     _odsPrinter << type;
  }
}
 
 
} // namespace llzk::verif
MLIR_DEFINE_EXPLICIT_TYPE_ID(::llzk::verif::ProveDetOp)
 
namespace llzk::verif {
 
 
//===----------------------------------------------------------------------===//
// ::llzk::verif::RequireComputeOp definitions
//===----------------------------------------------------------------------===//
 
namespace detail {
 
RequireComputeOpGenericAdaptorBase::RequireComputeOpGenericAdaptorBase(RequireComputeOp op) : odsAttrs(op->getRawDictionaryAttrs()), odsOpName(op->getName()), properties(op.getProperties()), odsRegions(op->getRegions()) {}
 
 
} // namespace detail
RequireComputeOpAdaptor::RequireComputeOpAdaptor(RequireComputeOp op) : RequireComputeOpGenericAdaptor(op->getOperands(), op) {}
 
::llvm::LogicalResult RequireComputeOpAdaptor::verify(::mlir::Location loc) {
  return ::mlir::success();
}
 
::llvm::LogicalResult RequireComputeOp::setPropertiesFromAttr(Properties &prop, ::mlir::Attribute attr, ::llvm::function_ref<::mlir::InFlightDiagnostic()> emitError) {
  ::mlir::DictionaryAttr dict = ::llvm::dyn_cast<::mlir::DictionaryAttr>(attr);
  if (!dict) {
    emitError() << "expected DictionaryAttr to set properties";
    return ::mlir::failure();
  }
      return ::mlir::success();
}
 
::mlir::Attribute RequireComputeOp::getPropertiesAsAttr(::mlir::MLIRContext *ctx, const Properties &prop) {
    ::mlir::SmallVector<::mlir::NamedAttribute> attrs;
    ::mlir::Builder odsBuilder{ctx};
 
  if (!attrs.empty())
    return odsBuilder.getDictionaryAttr(attrs);
  return {};
}
 
llvm::hash_code RequireComputeOp::computePropertiesHash(const Properties &prop) {
  using llvm::hash_value;
  return llvm::hash_combine();
}
 
std::optional<mlir::Attribute> RequireComputeOp::getInherentAttr(::mlir::MLIRContext *ctx, const Properties &prop, llvm::StringRef name) {
  return std::nullopt;
}
 
void RequireComputeOp::setInherentAttr(Properties &prop, llvm::StringRef name, mlir::Attribute value) {
}
 
void RequireComputeOp::populateInherentAttrs(::mlir::MLIRContext *ctx, const Properties &prop, ::mlir::NamedAttrList &attrs) {
}
 
::llvm::LogicalResult RequireComputeOp::verifyInherentAttrs(::mlir::OperationName opName, ::mlir::NamedAttrList &attrs, llvm::function_ref<::mlir::InFlightDiagnostic()> emitError) {
    return ::mlir::success();
}
 
void RequireComputeOp::build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, ::mlir::Value condition) {
  odsState.addOperands(condition);
}
 
RequireComputeOp RequireComputeOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::Value condition) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(condition)>(condition));
  auto __res__ = ::llvm::dyn_cast<RequireComputeOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
RequireComputeOp RequireComputeOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::Value condition) {
  return create(builder, builder.getLoc(), std::forward<decltype(condition)>(condition));
}
 
void RequireComputeOp::build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, ::mlir::TypeRange resultTypes, ::mlir::Value condition) {
  odsState.addOperands(condition);
  assert(resultTypes.size() == 0u && "mismatched number of results");
  odsState.addTypes(resultTypes);
}
 
RequireComputeOp RequireComputeOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::TypeRange resultTypes, ::mlir::Value condition) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(condition)>(condition));
  auto __res__ = ::llvm::dyn_cast<RequireComputeOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
RequireComputeOp RequireComputeOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::TypeRange resultTypes, ::mlir::Value condition) {
  return create(builder, builder.getLoc(), std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(condition)>(condition));
}
 
void RequireComputeOp::build(::mlir::OpBuilder &, ::mlir::OperationState &odsState, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, ::llvm::ArrayRef<::mlir::NamedAttribute> attributes) {
  assert(operands.size() == 1u && "mismatched number of parameters");
  odsState.addOperands(operands);
  odsState.addAttributes(attributes);
  assert(resultTypes.size() == 0u && "mismatched number of return types");
  odsState.addTypes(resultTypes);
}
 
RequireComputeOp RequireComputeOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, ::llvm::ArrayRef<::mlir::NamedAttribute> attributes) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(operands)>(operands), std::forward<decltype(attributes)>(attributes));
  auto __res__ = ::llvm::dyn_cast<RequireComputeOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
RequireComputeOp RequireComputeOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, ::llvm::ArrayRef<::mlir::NamedAttribute> attributes) {
  return create(builder, builder.getLoc(), std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(operands)>(operands), std::forward<decltype(attributes)>(attributes));
}
 
void RequireComputeOp::build(::mlir::OpBuilder &, ::mlir::OperationState &odsState, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, const Properties &properties, ::llvm::ArrayRef<::mlir::NamedAttribute> discardableAttributes) {
  assert(operands.size() == 1u && "mismatched number of parameters");
  odsState.addOperands(operands);
  odsState.useProperties(const_cast<Properties&>(properties));
  odsState.addAttributes(discardableAttributes);
  assert(resultTypes.size() == 0u && "mismatched number of return types");
  odsState.addTypes(resultTypes);
}
 
RequireComputeOp RequireComputeOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, const Properties &properties, ::llvm::ArrayRef<::mlir::NamedAttribute> discardableAttributes) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(operands)>(operands), std::forward<decltype(properties)>(properties), std::forward<decltype(discardableAttributes)>(discardableAttributes));
  auto __res__ = ::llvm::dyn_cast<RequireComputeOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
RequireComputeOp RequireComputeOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, const Properties &properties, ::llvm::ArrayRef<::mlir::NamedAttribute> discardableAttributes) {
  return create(builder, builder.getLoc(), std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(operands)>(operands), std::forward<decltype(properties)>(properties), std::forward<decltype(discardableAttributes)>(discardableAttributes));
}
 
::llvm::LogicalResult RequireComputeOp::verifyInvariantsImpl() {
  {
    unsigned index = 0; (void)index;
    auto valueGroup0 = getODSOperands(0);
 
    for (auto v : valueGroup0) {
      if (::mlir::failed(__mlir_ods_local_type_constraint_Ops3(*this, v.getType(), "operand", index++)))
        return ::mlir::failure();
    }
  }
  return ::mlir::success();
}
 
::llvm::LogicalResult RequireComputeOp::verifyInvariants() {
  return verifyInvariantsImpl();
}
 
::mlir::ParseResult RequireComputeOp::parse(::mlir::OpAsmParser &parser, ::mlir::OperationState &result) {
  ::mlir::OpAsmParser::UnresolvedOperand conditionRawOperand{};
  ::llvm::ArrayRef<::mlir::OpAsmParser::UnresolvedOperand> conditionOperands(&conditionRawOperand, 1);  ::llvm::SMLoc conditionOperandsLoc;
  (void)conditionOperandsLoc;
 
  conditionOperandsLoc = parser.getCurrentLocation();
  if (parser.parseOperand(conditionRawOperand))
    return ::mlir::failure();
  {
    auto loc = parser.getCurrentLocation();(void)loc;
    if (parser.parseOptionalAttrDict(result.attributes))
      return ::mlir::failure();
    if (failed(verifyInherentAttrs(result.name, result.attributes, [&]() {
        return parser.emitError(loc) << "'" << result.name.getStringRef() << "' op ";
      })))
      return ::mlir::failure();
  }
  ::mlir::Type odsBuildableType0 = parser.getBuilder().getIntegerType(1);
  if (parser.resolveOperands(conditionOperands, odsBuildableType0, conditionOperandsLoc, result.operands))
    return ::mlir::failure();
  return ::mlir::success();
}
 
void RequireComputeOp::print(::mlir::OpAsmPrinter &_odsPrinter) {
  _odsPrinter << ' ';
  _odsPrinter << getCondition();
  ::llvm::SmallVector<::llvm::StringRef, 2> elidedAttrs;
  _odsPrinter.printOptionalAttrDict((*this)->getAttrs(), elidedAttrs);
}
 
// This side effect models "program termination". Based on
// https://github.com/llvm/llvm-project/blob/f325e4b2d836d6e65a4d0cf3efc6b0996ccf3765/mlir/lib/Dialect/ControlFlow/IR/ControlFlowOps.cpp#L92-L97
void RequireComputeOp::getEffects(
    ::mlir::SmallVectorImpl<::mlir::SideEffects::EffectInstance<::mlir::MemoryEffects::Effect>> &effects
) {
  effects.emplace_back(::mlir::MemoryEffects::Write::get());
}
 
} // namespace llzk::verif
MLIR_DEFINE_EXPLICIT_TYPE_ID(::llzk::verif::RequireComputeOp)
 
namespace llzk::verif {
 
 
//===----------------------------------------------------------------------===//
// ::llzk::verif::RequireConstrainOp definitions
//===----------------------------------------------------------------------===//
 
namespace detail {
 
RequireConstrainOpGenericAdaptorBase::RequireConstrainOpGenericAdaptorBase(RequireConstrainOp op) : odsAttrs(op->getRawDictionaryAttrs()), odsOpName(op->getName()), properties(op.getProperties()), odsRegions(op->getRegions()) {}
 
 
} // namespace detail
RequireConstrainOpAdaptor::RequireConstrainOpAdaptor(RequireConstrainOp op) : RequireConstrainOpGenericAdaptor(op->getOperands(), op) {}
 
::llvm::LogicalResult RequireConstrainOpAdaptor::verify(::mlir::Location loc) {
  return ::mlir::success();
}
 
::llvm::LogicalResult RequireConstrainOp::setPropertiesFromAttr(Properties &prop, ::mlir::Attribute attr, ::llvm::function_ref<::mlir::InFlightDiagnostic()> emitError) {
  ::mlir::DictionaryAttr dict = ::llvm::dyn_cast<::mlir::DictionaryAttr>(attr);
  if (!dict) {
    emitError() << "expected DictionaryAttr to set properties";
    return ::mlir::failure();
  }
      return ::mlir::success();
}
 
::mlir::Attribute RequireConstrainOp::getPropertiesAsAttr(::mlir::MLIRContext *ctx, const Properties &prop) {
    ::mlir::SmallVector<::mlir::NamedAttribute> attrs;
    ::mlir::Builder odsBuilder{ctx};
 
  if (!attrs.empty())
    return odsBuilder.getDictionaryAttr(attrs);
  return {};
}
 
llvm::hash_code RequireConstrainOp::computePropertiesHash(const Properties &prop) {
  using llvm::hash_value;
  return llvm::hash_combine();
}
 
std::optional<mlir::Attribute> RequireConstrainOp::getInherentAttr(::mlir::MLIRContext *ctx, const Properties &prop, llvm::StringRef name) {
  return std::nullopt;
}
 
void RequireConstrainOp::setInherentAttr(Properties &prop, llvm::StringRef name, mlir::Attribute value) {
}
 
void RequireConstrainOp::populateInherentAttrs(::mlir::MLIRContext *ctx, const Properties &prop, ::mlir::NamedAttrList &attrs) {
}
 
::llvm::LogicalResult RequireConstrainOp::verifyInherentAttrs(::mlir::OperationName opName, ::mlir::NamedAttrList &attrs, llvm::function_ref<::mlir::InFlightDiagnostic()> emitError) {
    return ::mlir::success();
}
 
void RequireConstrainOp::build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, ::mlir::Value condition) {
  odsState.addOperands(condition);
}
 
RequireConstrainOp RequireConstrainOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::Value condition) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(condition)>(condition));
  auto __res__ = ::llvm::dyn_cast<RequireConstrainOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
RequireConstrainOp RequireConstrainOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::Value condition) {
  return create(builder, builder.getLoc(), std::forward<decltype(condition)>(condition));
}
 
void RequireConstrainOp::build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, ::mlir::TypeRange resultTypes, ::mlir::Value condition) {
  odsState.addOperands(condition);
  assert(resultTypes.size() == 0u && "mismatched number of results");
  odsState.addTypes(resultTypes);
}
 
RequireConstrainOp RequireConstrainOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::TypeRange resultTypes, ::mlir::Value condition) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(condition)>(condition));
  auto __res__ = ::llvm::dyn_cast<RequireConstrainOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
RequireConstrainOp RequireConstrainOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::TypeRange resultTypes, ::mlir::Value condition) {
  return create(builder, builder.getLoc(), std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(condition)>(condition));
}
 
void RequireConstrainOp::build(::mlir::OpBuilder &, ::mlir::OperationState &odsState, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, ::llvm::ArrayRef<::mlir::NamedAttribute> attributes) {
  assert(operands.size() == 1u && "mismatched number of parameters");
  odsState.addOperands(operands);
  odsState.addAttributes(attributes);
  assert(resultTypes.size() == 0u && "mismatched number of return types");
  odsState.addTypes(resultTypes);
}
 
RequireConstrainOp RequireConstrainOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, ::llvm::ArrayRef<::mlir::NamedAttribute> attributes) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(operands)>(operands), std::forward<decltype(attributes)>(attributes));
  auto __res__ = ::llvm::dyn_cast<RequireConstrainOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
RequireConstrainOp RequireConstrainOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, ::llvm::ArrayRef<::mlir::NamedAttribute> attributes) {
  return create(builder, builder.getLoc(), std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(operands)>(operands), std::forward<decltype(attributes)>(attributes));
}
 
void RequireConstrainOp::build(::mlir::OpBuilder &, ::mlir::OperationState &odsState, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, const Properties &properties, ::llvm::ArrayRef<::mlir::NamedAttribute> discardableAttributes) {
  assert(operands.size() == 1u && "mismatched number of parameters");
  odsState.addOperands(operands);
  odsState.useProperties(const_cast<Properties&>(properties));
  odsState.addAttributes(discardableAttributes);
  assert(resultTypes.size() == 0u && "mismatched number of return types");
  odsState.addTypes(resultTypes);
}
 
RequireConstrainOp RequireConstrainOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, const Properties &properties, ::llvm::ArrayRef<::mlir::NamedAttribute> discardableAttributes) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(operands)>(operands), std::forward<decltype(properties)>(properties), std::forward<decltype(discardableAttributes)>(discardableAttributes));
  auto __res__ = ::llvm::dyn_cast<RequireConstrainOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
RequireConstrainOp RequireConstrainOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, const Properties &properties, ::llvm::ArrayRef<::mlir::NamedAttribute> discardableAttributes) {
  return create(builder, builder.getLoc(), std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(operands)>(operands), std::forward<decltype(properties)>(properties), std::forward<decltype(discardableAttributes)>(discardableAttributes));
}
 
::llvm::LogicalResult RequireConstrainOp::verifyInvariantsImpl() {
  {
    unsigned index = 0; (void)index;
    auto valueGroup0 = getODSOperands(0);
 
    for (auto v : valueGroup0) {
      if (::mlir::failed(__mlir_ods_local_type_constraint_Ops3(*this, v.getType(), "operand", index++)))
        return ::mlir::failure();
    }
  }
  return ::mlir::success();
}
 
::llvm::LogicalResult RequireConstrainOp::verifyInvariants() {
  return verifyInvariantsImpl();
}
 
::mlir::ParseResult RequireConstrainOp::parse(::mlir::OpAsmParser &parser, ::mlir::OperationState &result) {
  ::mlir::OpAsmParser::UnresolvedOperand conditionRawOperand{};
  ::llvm::ArrayRef<::mlir::OpAsmParser::UnresolvedOperand> conditionOperands(&conditionRawOperand, 1);  ::llvm::SMLoc conditionOperandsLoc;
  (void)conditionOperandsLoc;
 
  conditionOperandsLoc = parser.getCurrentLocation();
  if (parser.parseOperand(conditionRawOperand))
    return ::mlir::failure();
  {
    auto loc = parser.getCurrentLocation();(void)loc;
    if (parser.parseOptionalAttrDict(result.attributes))
      return ::mlir::failure();
    if (failed(verifyInherentAttrs(result.name, result.attributes, [&]() {
        return parser.emitError(loc) << "'" << result.name.getStringRef() << "' op ";
      })))
      return ::mlir::failure();
  }
  ::mlir::Type odsBuildableType0 = parser.getBuilder().getIntegerType(1);
  if (parser.resolveOperands(conditionOperands, odsBuildableType0, conditionOperandsLoc, result.operands))
    return ::mlir::failure();
  return ::mlir::success();
}
 
void RequireConstrainOp::print(::mlir::OpAsmPrinter &_odsPrinter) {
  _odsPrinter << ' ';
  _odsPrinter << getCondition();
  ::llvm::SmallVector<::llvm::StringRef, 2> elidedAttrs;
  _odsPrinter.printOptionalAttrDict((*this)->getAttrs(), elidedAttrs);
}
 
// This side effect models "program termination". Based on
// https://github.com/llvm/llvm-project/blob/f325e4b2d836d6e65a4d0cf3efc6b0996ccf3765/mlir/lib/Dialect/ControlFlow/IR/ControlFlowOps.cpp#L92-L97
void RequireConstrainOp::getEffects(
    ::mlir::SmallVectorImpl<::mlir::SideEffects::EffectInstance<::mlir::MemoryEffects::Effect>> &effects
) {
  effects.emplace_back(::mlir::MemoryEffects::Write::get());
}
 
} // namespace llzk::verif
MLIR_DEFINE_EXPLICIT_TYPE_ID(::llzk::verif::RequireConstrainOp)
 
namespace llzk::verif {
 
 
//===----------------------------------------------------------------------===//
// ::llzk::verif::StepOp definitions
//===----------------------------------------------------------------------===//
 
namespace detail {
 
StepOpGenericAdaptorBase::StepOpGenericAdaptorBase(StepOp op) : odsAttrs(op->getRawDictionaryAttrs()), odsOpName(op->getName()), properties(op.getProperties()), odsRegions(op->getRegions()) {}
 
 
} // namespace detail
StepOpAdaptor::StepOpAdaptor(StepOp op) : StepOpGenericAdaptor(op->getOperands(), op) {}
 
::llvm::LogicalResult StepOpAdaptor::verify(::mlir::Location loc) {
  return ::mlir::success();
}
 
::llvm::LogicalResult StepOp::setPropertiesFromAttr(Properties &prop, ::mlir::Attribute attr, ::llvm::function_ref<::mlir::InFlightDiagnostic()> emitError) {
  ::mlir::DictionaryAttr dict = ::llvm::dyn_cast<::mlir::DictionaryAttr>(attr);
  if (!dict) {
    emitError() << "expected DictionaryAttr to set properties";
    return ::mlir::failure();
  }
      return ::mlir::success();
}
 
::mlir::Attribute StepOp::getPropertiesAsAttr(::mlir::MLIRContext *ctx, const Properties &prop) {
    ::mlir::SmallVector<::mlir::NamedAttribute> attrs;
    ::mlir::Builder odsBuilder{ctx};
 
  if (!attrs.empty())
    return odsBuilder.getDictionaryAttr(attrs);
  return {};
}
 
llvm::hash_code StepOp::computePropertiesHash(const Properties &prop) {
  using llvm::hash_value;
  return llvm::hash_combine();
}
 
std::optional<mlir::Attribute> StepOp::getInherentAttr(::mlir::MLIRContext *ctx, const Properties &prop, llvm::StringRef name) {
  return std::nullopt;
}
 
void StepOp::setInherentAttr(Properties &prop, llvm::StringRef name, mlir::Attribute value) {
}
 
void StepOp::populateInherentAttrs(::mlir::MLIRContext *ctx, const Properties &prop, ::mlir::NamedAttrList &attrs) {
}
 
::llvm::LogicalResult StepOp::verifyInherentAttrs(::mlir::OperationName opName, ::mlir::NamedAttrList &attrs, llvm::function_ref<::mlir::InFlightDiagnostic()> emitError) {
    return ::mlir::success();
}
 
void StepOp::build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState) {
  (void)odsState.addRegion();
}
 
StepOp StepOp::create(::mlir::OpBuilder &builder, ::mlir::Location location) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__);
  auto __res__ = ::llvm::dyn_cast<StepOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
StepOp StepOp::create(::mlir::ImplicitLocOpBuilder &builder) {
  return create(builder, builder.getLoc());
}
 
void StepOp::build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, ::mlir::TypeRange resultTypes) {
  (void)odsState.addRegion();
  assert(resultTypes.size() == 0u && "mismatched number of results");
  odsState.addTypes(resultTypes);
}
 
StepOp StepOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::TypeRange resultTypes) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(resultTypes)>(resultTypes));
  auto __res__ = ::llvm::dyn_cast<StepOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
StepOp StepOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::TypeRange resultTypes) {
  return create(builder, builder.getLoc(), std::forward<decltype(resultTypes)>(resultTypes));
}
 
void StepOp::build(::mlir::OpBuilder &, ::mlir::OperationState &odsState, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, ::llvm::ArrayRef<::mlir::NamedAttribute> attributes) {
  assert(operands.size() == 0u && "mismatched number of parameters");
  odsState.addOperands(operands);
  odsState.addAttributes(attributes);
  for (unsigned i = 0; i != 1; ++i)
    (void)odsState.addRegion();
  assert(resultTypes.size() == 0u && "mismatched number of return types");
  odsState.addTypes(resultTypes);
}
 
StepOp StepOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, ::llvm::ArrayRef<::mlir::NamedAttribute> attributes) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(operands)>(operands), std::forward<decltype(attributes)>(attributes));
  auto __res__ = ::llvm::dyn_cast<StepOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
StepOp StepOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, ::llvm::ArrayRef<::mlir::NamedAttribute> attributes) {
  return create(builder, builder.getLoc(), std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(operands)>(operands), std::forward<decltype(attributes)>(attributes));
}
 
void StepOp::build(::mlir::OpBuilder &, ::mlir::OperationState &odsState, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, const Properties &properties, ::llvm::ArrayRef<::mlir::NamedAttribute> discardableAttributes) {
  assert(operands.size() == 0u && "mismatched number of parameters");
  odsState.addOperands(operands);
  odsState.useProperties(const_cast<Properties&>(properties));
  odsState.addAttributes(discardableAttributes);
  for (unsigned i = 0; i != 1; ++i)
    (void)odsState.addRegion();
  assert(resultTypes.size() == 0u && "mismatched number of return types");
  odsState.addTypes(resultTypes);
}
 
StepOp StepOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, const Properties &properties, ::llvm::ArrayRef<::mlir::NamedAttribute> discardableAttributes) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(operands)>(operands), std::forward<decltype(properties)>(properties), std::forward<decltype(discardableAttributes)>(discardableAttributes));
  auto __res__ = ::llvm::dyn_cast<StepOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
StepOp StepOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, const Properties &properties, ::llvm::ArrayRef<::mlir::NamedAttribute> discardableAttributes) {
  return create(builder, builder.getLoc(), std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(operands)>(operands), std::forward<decltype(properties)>(properties), std::forward<decltype(discardableAttributes)>(discardableAttributes));
}
 
::llvm::LogicalResult StepOp::verifyInvariantsImpl() {
  {
    unsigned index = 0; (void)index;
 
    for (auto &region : ::llvm::MutableArrayRef((*this)->getRegion(0)))
      if (::mlir::failed(__mlir_ods_local_region_constraint_Ops2(*this, region, "region", index++)))
        return ::mlir::failure();
  }
  return ::mlir::success();
}
 
::llvm::LogicalResult StepOp::verifyInvariants() {
  return verifyInvariantsImpl();
}
 
::mlir::ParseResult StepOp::parse(::mlir::OpAsmParser &parser, ::mlir::OperationState &result) {
  std::unique_ptr<::mlir::Region> regionRegion = std::make_unique<::mlir::Region>();
 
  if (parser.parseRegion(*regionRegion))
    return ::mlir::failure();
 
  if (regionRegion->empty()) regionRegion->emplaceBlock();
  {
    auto loc = parser.getCurrentLocation();(void)loc;
    if (parser.parseOptionalAttrDict(result.attributes))
      return ::mlir::failure();
    if (failed(verifyInherentAttrs(result.name, result.attributes, [&]() {
        return parser.emitError(loc) << "'" << result.name.getStringRef() << "' op ";
      })))
      return ::mlir::failure();
  }
  result.addRegion(std::move(regionRegion));
  return ::mlir::success();
}
 
void StepOp::print(::mlir::OpAsmPrinter &_odsPrinter) {
  _odsPrinter << ' ';
  _odsPrinter.printRegion(getRegion());
  ::llvm::SmallVector<::llvm::StringRef, 2> elidedAttrs;
  _odsPrinter.printOptionalAttrDict((*this)->getAttrs(), elidedAttrs);
}
 
// This side effect models "program termination". Based on
// https://github.com/llvm/llvm-project/blob/f325e4b2d836d6e65a4d0cf3efc6b0996ccf3765/mlir/lib/Dialect/ControlFlow/IR/ControlFlowOps.cpp#L92-L97
void StepOp::getEffects(
    ::mlir::SmallVectorImpl<::mlir::SideEffects::EffectInstance<::mlir::MemoryEffects::Effect>> &effects
) {
  effects.emplace_back(::mlir::MemoryEffects::Write::get());
}
 
} // namespace llzk::verif
MLIR_DEFINE_EXPLICIT_TYPE_ID(::llzk::verif::StepOp)
 
namespace llzk::verif {
 
 
//===----------------------------------------------------------------------===//
// ::llzk::verif::StepYieldOp definitions
//===----------------------------------------------------------------------===//
 
namespace detail {
 
StepYieldOpGenericAdaptorBase::StepYieldOpGenericAdaptorBase(StepYieldOp op) : odsAttrs(op->getRawDictionaryAttrs()), odsOpName(op->getName()), properties(op.getProperties()), odsRegions(op->getRegions()) {}
 
 
} // namespace detail
StepYieldOpAdaptor::StepYieldOpAdaptor(StepYieldOp op) : StepYieldOpGenericAdaptor(op->getOperands(), op) {}
 
::llvm::LogicalResult StepYieldOpAdaptor::verify(::mlir::Location loc) {
  return ::mlir::success();
}
 
::llvm::LogicalResult StepYieldOp::setPropertiesFromAttr(Properties &prop, ::mlir::Attribute attr, ::llvm::function_ref<::mlir::InFlightDiagnostic()> emitError) {
  ::mlir::DictionaryAttr dict = ::llvm::dyn_cast<::mlir::DictionaryAttr>(attr);
  if (!dict) {
    emitError() << "expected DictionaryAttr to set properties";
    return ::mlir::failure();
  }
      return ::mlir::success();
}
 
::mlir::Attribute StepYieldOp::getPropertiesAsAttr(::mlir::MLIRContext *ctx, const Properties &prop) {
    ::mlir::SmallVector<::mlir::NamedAttribute> attrs;
    ::mlir::Builder odsBuilder{ctx};
 
  if (!attrs.empty())
    return odsBuilder.getDictionaryAttr(attrs);
  return {};
}
 
llvm::hash_code StepYieldOp::computePropertiesHash(const Properties &prop) {
  using llvm::hash_value;
  return llvm::hash_combine();
}
 
std::optional<mlir::Attribute> StepYieldOp::getInherentAttr(::mlir::MLIRContext *ctx, const Properties &prop, llvm::StringRef name) {
  return std::nullopt;
}
 
void StepYieldOp::setInherentAttr(Properties &prop, llvm::StringRef name, mlir::Attribute value) {
}
 
void StepYieldOp::populateInherentAttrs(::mlir::MLIRContext *ctx, const Properties &prop, ::mlir::NamedAttrList &attrs) {
}
 
::llvm::LogicalResult StepYieldOp::verifyInherentAttrs(::mlir::OperationName opName, ::mlir::NamedAttrList &attrs, llvm::function_ref<::mlir::InFlightDiagnostic()> emitError) {
    return ::mlir::success();
}
 
void StepYieldOp::build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, ::mlir::Value value) {
  odsState.addOperands(value);
}
 
StepYieldOp StepYieldOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::Value value) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(value)>(value));
  auto __res__ = ::llvm::dyn_cast<StepYieldOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
StepYieldOp StepYieldOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::Value value) {
  return create(builder, builder.getLoc(), std::forward<decltype(value)>(value));
}
 
void StepYieldOp::build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, ::mlir::TypeRange resultTypes, ::mlir::Value value) {
  odsState.addOperands(value);
  assert(resultTypes.size() == 0u && "mismatched number of results");
  odsState.addTypes(resultTypes);
}
 
StepYieldOp StepYieldOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::TypeRange resultTypes, ::mlir::Value value) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(value)>(value));
  auto __res__ = ::llvm::dyn_cast<StepYieldOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
StepYieldOp StepYieldOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::TypeRange resultTypes, ::mlir::Value value) {
  return create(builder, builder.getLoc(), std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(value)>(value));
}
 
void StepYieldOp::build(::mlir::OpBuilder &, ::mlir::OperationState &odsState, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, ::llvm::ArrayRef<::mlir::NamedAttribute> attributes) {
  assert(operands.size() == 1u && "mismatched number of parameters");
  odsState.addOperands(operands);
  odsState.addAttributes(attributes);
  assert(resultTypes.size() == 0u && "mismatched number of return types");
  odsState.addTypes(resultTypes);
}
 
StepYieldOp StepYieldOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, ::llvm::ArrayRef<::mlir::NamedAttribute> attributes) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(operands)>(operands), std::forward<decltype(attributes)>(attributes));
  auto __res__ = ::llvm::dyn_cast<StepYieldOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
StepYieldOp StepYieldOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, ::llvm::ArrayRef<::mlir::NamedAttribute> attributes) {
  return create(builder, builder.getLoc(), std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(operands)>(operands), std::forward<decltype(attributes)>(attributes));
}
 
void StepYieldOp::build(::mlir::OpBuilder &, ::mlir::OperationState &odsState, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, const Properties &properties, ::llvm::ArrayRef<::mlir::NamedAttribute> discardableAttributes) {
  assert(operands.size() == 1u && "mismatched number of parameters");
  odsState.addOperands(operands);
  odsState.useProperties(const_cast<Properties&>(properties));
  odsState.addAttributes(discardableAttributes);
  assert(resultTypes.size() == 0u && "mismatched number of return types");
  odsState.addTypes(resultTypes);
}
 
StepYieldOp StepYieldOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, const Properties &properties, ::llvm::ArrayRef<::mlir::NamedAttribute> discardableAttributes) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(operands)>(operands), std::forward<decltype(properties)>(properties), std::forward<decltype(discardableAttributes)>(discardableAttributes));
  auto __res__ = ::llvm::dyn_cast<StepYieldOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
StepYieldOp StepYieldOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, const Properties &properties, ::llvm::ArrayRef<::mlir::NamedAttribute> discardableAttributes) {
  return create(builder, builder.getLoc(), std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(operands)>(operands), std::forward<decltype(properties)>(properties), std::forward<decltype(discardableAttributes)>(discardableAttributes));
}
 
::llvm::LogicalResult StepYieldOp::verifyInvariantsImpl() {
  {
    unsigned index = 0; (void)index;
    auto valueGroup0 = getODSOperands(0);
 
    for (auto v : valueGroup0) {
      if (::mlir::failed(__mlir_ods_local_type_constraint_Ops3(*this, v.getType(), "operand", index++)))
        return ::mlir::failure();
    }
  }
  return ::mlir::success();
}
 
::llvm::LogicalResult StepYieldOp::verifyInvariants() {
  return verifyInvariantsImpl();
}
 
::mlir::ParseResult StepYieldOp::parse(::mlir::OpAsmParser &parser, ::mlir::OperationState &result) {
  ::mlir::OpAsmParser::UnresolvedOperand valueRawOperand{};
  ::llvm::ArrayRef<::mlir::OpAsmParser::UnresolvedOperand> valueOperands(&valueRawOperand, 1);  ::llvm::SMLoc valueOperandsLoc;
  (void)valueOperandsLoc;
 
  valueOperandsLoc = parser.getCurrentLocation();
  if (parser.parseOperand(valueRawOperand))
    return ::mlir::failure();
  {
    auto loc = parser.getCurrentLocation();(void)loc;
    if (parser.parseOptionalAttrDict(result.attributes))
      return ::mlir::failure();
    if (failed(verifyInherentAttrs(result.name, result.attributes, [&]() {
        return parser.emitError(loc) << "'" << result.name.getStringRef() << "' op ";
      })))
      return ::mlir::failure();
  }
  ::mlir::Type odsBuildableType0 = parser.getBuilder().getIntegerType(1);
  if (parser.resolveOperands(valueOperands, odsBuildableType0, valueOperandsLoc, result.operands))
    return ::mlir::failure();
  return ::mlir::success();
}
 
void StepYieldOp::print(::mlir::OpAsmPrinter &_odsPrinter) {
  _odsPrinter << ' ';
  _odsPrinter << getValue();
  ::llvm::SmallVector<::llvm::StringRef, 2> elidedAttrs;
  _odsPrinter.printOptionalAttrDict((*this)->getAttrs(), elidedAttrs);
}
 
 
} // namespace llzk::verif
MLIR_DEFINE_EXPLICIT_TYPE_ID(::llzk::verif::StepYieldOp)
 
namespace llzk::verif {
 
 
//===----------------------------------------------------------------------===//
// ::llzk::verif::VerifAssertOp definitions
//===----------------------------------------------------------------------===//
 
namespace detail {
 
VerifAssertOpGenericAdaptorBase::VerifAssertOpGenericAdaptorBase(VerifAssertOp op) : odsAttrs(op->getRawDictionaryAttrs()), odsOpName(op->getName()), properties(op.getProperties()), odsRegions(op->getRegions()) {}
 
 
} // namespace detail
VerifAssertOpAdaptor::VerifAssertOpAdaptor(VerifAssertOp op) : VerifAssertOpGenericAdaptor(op->getOperands(), op) {}
 
::llvm::LogicalResult VerifAssertOpAdaptor::verify(::mlir::Location loc) {
  return ::mlir::success();
}
 
::llvm::LogicalResult VerifAssertOp::setPropertiesFromAttr(Properties &prop, ::mlir::Attribute attr, ::llvm::function_ref<::mlir::InFlightDiagnostic()> emitError) {
  ::mlir::DictionaryAttr dict = ::llvm::dyn_cast<::mlir::DictionaryAttr>(attr);
  if (!dict) {
    emitError() << "expected DictionaryAttr to set properties";
    return ::mlir::failure();
  }
      return ::mlir::success();
}
 
::mlir::Attribute VerifAssertOp::getPropertiesAsAttr(::mlir::MLIRContext *ctx, const Properties &prop) {
    ::mlir::SmallVector<::mlir::NamedAttribute> attrs;
    ::mlir::Builder odsBuilder{ctx};
 
  if (!attrs.empty())
    return odsBuilder.getDictionaryAttr(attrs);
  return {};
}
 
llvm::hash_code VerifAssertOp::computePropertiesHash(const Properties &prop) {
  using llvm::hash_value;
  return llvm::hash_combine();
}
 
std::optional<mlir::Attribute> VerifAssertOp::getInherentAttr(::mlir::MLIRContext *ctx, const Properties &prop, llvm::StringRef name) {
  return std::nullopt;
}
 
void VerifAssertOp::setInherentAttr(Properties &prop, llvm::StringRef name, mlir::Attribute value) {
}
 
void VerifAssertOp::populateInherentAttrs(::mlir::MLIRContext *ctx, const Properties &prop, ::mlir::NamedAttrList &attrs) {
}
 
::llvm::LogicalResult VerifAssertOp::verifyInherentAttrs(::mlir::OperationName opName, ::mlir::NamedAttrList &attrs, llvm::function_ref<::mlir::InFlightDiagnostic()> emitError) {
    return ::mlir::success();
}
 
void VerifAssertOp::build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, ::mlir::Value condition) {
  odsState.addOperands(condition);
}
 
VerifAssertOp VerifAssertOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::Value condition) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(condition)>(condition));
  auto __res__ = ::llvm::dyn_cast<VerifAssertOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
VerifAssertOp VerifAssertOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::Value condition) {
  return create(builder, builder.getLoc(), std::forward<decltype(condition)>(condition));
}
 
void VerifAssertOp::build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, ::mlir::TypeRange resultTypes, ::mlir::Value condition) {
  odsState.addOperands(condition);
  assert(resultTypes.size() == 0u && "mismatched number of results");
  odsState.addTypes(resultTypes);
}
 
VerifAssertOp VerifAssertOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::TypeRange resultTypes, ::mlir::Value condition) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(condition)>(condition));
  auto __res__ = ::llvm::dyn_cast<VerifAssertOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
VerifAssertOp VerifAssertOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::TypeRange resultTypes, ::mlir::Value condition) {
  return create(builder, builder.getLoc(), std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(condition)>(condition));
}
 
void VerifAssertOp::build(::mlir::OpBuilder &, ::mlir::OperationState &odsState, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, ::llvm::ArrayRef<::mlir::NamedAttribute> attributes) {
  assert(operands.size() == 1u && "mismatched number of parameters");
  odsState.addOperands(operands);
  odsState.addAttributes(attributes);
  assert(resultTypes.size() == 0u && "mismatched number of return types");
  odsState.addTypes(resultTypes);
}
 
VerifAssertOp VerifAssertOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, ::llvm::ArrayRef<::mlir::NamedAttribute> attributes) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(operands)>(operands), std::forward<decltype(attributes)>(attributes));
  auto __res__ = ::llvm::dyn_cast<VerifAssertOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
VerifAssertOp VerifAssertOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, ::llvm::ArrayRef<::mlir::NamedAttribute> attributes) {
  return create(builder, builder.getLoc(), std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(operands)>(operands), std::forward<decltype(attributes)>(attributes));
}
 
void VerifAssertOp::build(::mlir::OpBuilder &, ::mlir::OperationState &odsState, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, const Properties &properties, ::llvm::ArrayRef<::mlir::NamedAttribute> discardableAttributes) {
  assert(operands.size() == 1u && "mismatched number of parameters");
  odsState.addOperands(operands);
  odsState.useProperties(const_cast<Properties&>(properties));
  odsState.addAttributes(discardableAttributes);
  assert(resultTypes.size() == 0u && "mismatched number of return types");
  odsState.addTypes(resultTypes);
}
 
VerifAssertOp VerifAssertOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, const Properties &properties, ::llvm::ArrayRef<::mlir::NamedAttribute> discardableAttributes) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(operands)>(operands), std::forward<decltype(properties)>(properties), std::forward<decltype(discardableAttributes)>(discardableAttributes));
  auto __res__ = ::llvm::dyn_cast<VerifAssertOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
VerifAssertOp VerifAssertOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, const Properties &properties, ::llvm::ArrayRef<::mlir::NamedAttribute> discardableAttributes) {
  return create(builder, builder.getLoc(), std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(operands)>(operands), std::forward<decltype(properties)>(properties), std::forward<decltype(discardableAttributes)>(discardableAttributes));
}
 
::llvm::LogicalResult VerifAssertOp::verifyInvariantsImpl() {
  {
    unsigned index = 0; (void)index;
    auto valueGroup0 = getODSOperands(0);
 
    for (auto v : valueGroup0) {
      if (::mlir::failed(__mlir_ods_local_type_constraint_Ops3(*this, v.getType(), "operand", index++)))
        return ::mlir::failure();
    }
  }
  return ::mlir::success();
}
 
::llvm::LogicalResult VerifAssertOp::verifyInvariants() {
  return verifyInvariantsImpl();
}
 
::mlir::ParseResult VerifAssertOp::parse(::mlir::OpAsmParser &parser, ::mlir::OperationState &result) {
  ::mlir::OpAsmParser::UnresolvedOperand conditionRawOperand{};
  ::llvm::ArrayRef<::mlir::OpAsmParser::UnresolvedOperand> conditionOperands(&conditionRawOperand, 1);  ::llvm::SMLoc conditionOperandsLoc;
  (void)conditionOperandsLoc;
 
  conditionOperandsLoc = parser.getCurrentLocation();
  if (parser.parseOperand(conditionRawOperand))
    return ::mlir::failure();
  {
    auto loc = parser.getCurrentLocation();(void)loc;
    if (parser.parseOptionalAttrDict(result.attributes))
      return ::mlir::failure();
    if (failed(verifyInherentAttrs(result.name, result.attributes, [&]() {
        return parser.emitError(loc) << "'" << result.name.getStringRef() << "' op ";
      })))
      return ::mlir::failure();
  }
  ::mlir::Type odsBuildableType0 = parser.getBuilder().getIntegerType(1);
  if (parser.resolveOperands(conditionOperands, odsBuildableType0, conditionOperandsLoc, result.operands))
    return ::mlir::failure();
  return ::mlir::success();
}
 
void VerifAssertOp::print(::mlir::OpAsmPrinter &_odsPrinter) {
  _odsPrinter << ' ';
  _odsPrinter << getCondition();
  ::llvm::SmallVector<::llvm::StringRef, 2> elidedAttrs;
  _odsPrinter.printOptionalAttrDict((*this)->getAttrs(), elidedAttrs);
}
 
// This side effect models "program termination". Based on
// https://github.com/llvm/llvm-project/blob/f325e4b2d836d6e65a4d0cf3efc6b0996ccf3765/mlir/lib/Dialect/ControlFlow/IR/ControlFlowOps.cpp#L92-L97
void VerifAssertOp::getEffects(
    ::mlir::SmallVectorImpl<::mlir::SideEffects::EffectInstance<::mlir::MemoryEffects::Effect>> &effects
) {
  effects.emplace_back(::mlir::MemoryEffects::Write::get());
}
 
} // namespace llzk::verif
MLIR_DEFINE_EXPLICIT_TYPE_ID(::llzk::verif::VerifAssertOp)
 
namespace llzk::verif {
 
 
//===----------------------------------------------------------------------===//
// ::llzk::verif::VerifProveOp definitions
//===----------------------------------------------------------------------===//
 
namespace detail {
 
VerifProveOpGenericAdaptorBase::VerifProveOpGenericAdaptorBase(VerifProveOp op) : odsAttrs(op->getRawDictionaryAttrs()), odsOpName(op->getName()), properties(op.getProperties()), odsRegions(op->getRegions()) {}
 
 
} // namespace detail
VerifProveOpAdaptor::VerifProveOpAdaptor(VerifProveOp op) : VerifProveOpGenericAdaptor(op->getOperands(), op) {}
 
::llvm::LogicalResult VerifProveOpAdaptor::verify(::mlir::Location loc) {
  return ::mlir::success();
}
 
::llvm::LogicalResult VerifProveOp::setPropertiesFromAttr(Properties &prop, ::mlir::Attribute attr, ::llvm::function_ref<::mlir::InFlightDiagnostic()> emitError) {
  ::mlir::DictionaryAttr dict = ::llvm::dyn_cast<::mlir::DictionaryAttr>(attr);
  if (!dict) {
    emitError() << "expected DictionaryAttr to set properties";
    return ::mlir::failure();
  }
      return ::mlir::success();
}
 
::mlir::Attribute VerifProveOp::getPropertiesAsAttr(::mlir::MLIRContext *ctx, const Properties &prop) {
    ::mlir::SmallVector<::mlir::NamedAttribute> attrs;
    ::mlir::Builder odsBuilder{ctx};
 
  if (!attrs.empty())
    return odsBuilder.getDictionaryAttr(attrs);
  return {};
}
 
llvm::hash_code VerifProveOp::computePropertiesHash(const Properties &prop) {
  using llvm::hash_value;
  return llvm::hash_combine();
}
 
std::optional<mlir::Attribute> VerifProveOp::getInherentAttr(::mlir::MLIRContext *ctx, const Properties &prop, llvm::StringRef name) {
  return std::nullopt;
}
 
void VerifProveOp::setInherentAttr(Properties &prop, llvm::StringRef name, mlir::Attribute value) {
}
 
void VerifProveOp::populateInherentAttrs(::mlir::MLIRContext *ctx, const Properties &prop, ::mlir::NamedAttrList &attrs) {
}
 
::llvm::LogicalResult VerifProveOp::verifyInherentAttrs(::mlir::OperationName opName, ::mlir::NamedAttrList &attrs, llvm::function_ref<::mlir::InFlightDiagnostic()> emitError) {
    return ::mlir::success();
}
 
void VerifProveOp::build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, ::mlir::Value condition) {
  odsState.addOperands(condition);
}
 
VerifProveOp VerifProveOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::Value condition) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(condition)>(condition));
  auto __res__ = ::llvm::dyn_cast<VerifProveOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
VerifProveOp VerifProveOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::Value condition) {
  return create(builder, builder.getLoc(), std::forward<decltype(condition)>(condition));
}
 
void VerifProveOp::build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, ::mlir::TypeRange resultTypes, ::mlir::Value condition) {
  odsState.addOperands(condition);
  assert(resultTypes.size() == 0u && "mismatched number of results");
  odsState.addTypes(resultTypes);
}
 
VerifProveOp VerifProveOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::TypeRange resultTypes, ::mlir::Value condition) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(condition)>(condition));
  auto __res__ = ::llvm::dyn_cast<VerifProveOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
VerifProveOp VerifProveOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::TypeRange resultTypes, ::mlir::Value condition) {
  return create(builder, builder.getLoc(), std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(condition)>(condition));
}
 
void VerifProveOp::build(::mlir::OpBuilder &, ::mlir::OperationState &odsState, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, ::llvm::ArrayRef<::mlir::NamedAttribute> attributes) {
  assert(operands.size() == 1u && "mismatched number of parameters");
  odsState.addOperands(operands);
  odsState.addAttributes(attributes);
  assert(resultTypes.size() == 0u && "mismatched number of return types");
  odsState.addTypes(resultTypes);
}
 
VerifProveOp VerifProveOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, ::llvm::ArrayRef<::mlir::NamedAttribute> attributes) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(operands)>(operands), std::forward<decltype(attributes)>(attributes));
  auto __res__ = ::llvm::dyn_cast<VerifProveOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
VerifProveOp VerifProveOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, ::llvm::ArrayRef<::mlir::NamedAttribute> attributes) {
  return create(builder, builder.getLoc(), std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(operands)>(operands), std::forward<decltype(attributes)>(attributes));
}
 
void VerifProveOp::build(::mlir::OpBuilder &, ::mlir::OperationState &odsState, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, const Properties &properties, ::llvm::ArrayRef<::mlir::NamedAttribute> discardableAttributes) {
  assert(operands.size() == 1u && "mismatched number of parameters");
  odsState.addOperands(operands);
  odsState.useProperties(const_cast<Properties&>(properties));
  odsState.addAttributes(discardableAttributes);
  assert(resultTypes.size() == 0u && "mismatched number of return types");
  odsState.addTypes(resultTypes);
}
 
VerifProveOp VerifProveOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, const Properties &properties, ::llvm::ArrayRef<::mlir::NamedAttribute> discardableAttributes) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(operands)>(operands), std::forward<decltype(properties)>(properties), std::forward<decltype(discardableAttributes)>(discardableAttributes));
  auto __res__ = ::llvm::dyn_cast<VerifProveOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
VerifProveOp VerifProveOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, const Properties &properties, ::llvm::ArrayRef<::mlir::NamedAttribute> discardableAttributes) {
  return create(builder, builder.getLoc(), std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(operands)>(operands), std::forward<decltype(properties)>(properties), std::forward<decltype(discardableAttributes)>(discardableAttributes));
}
 
::llvm::LogicalResult VerifProveOp::verifyInvariantsImpl() {
  {
    unsigned index = 0; (void)index;
    auto valueGroup0 = getODSOperands(0);
 
    for (auto v : valueGroup0) {
      if (::mlir::failed(__mlir_ods_local_type_constraint_Ops3(*this, v.getType(), "operand", index++)))
        return ::mlir::failure();
    }
  }
  return ::mlir::success();
}
 
::llvm::LogicalResult VerifProveOp::verifyInvariants() {
  return verifyInvariantsImpl();
}
 
::mlir::ParseResult VerifProveOp::parse(::mlir::OpAsmParser &parser, ::mlir::OperationState &result) {
  ::mlir::OpAsmParser::UnresolvedOperand conditionRawOperand{};
  ::llvm::ArrayRef<::mlir::OpAsmParser::UnresolvedOperand> conditionOperands(&conditionRawOperand, 1);  ::llvm::SMLoc conditionOperandsLoc;
  (void)conditionOperandsLoc;
 
  conditionOperandsLoc = parser.getCurrentLocation();
  if (parser.parseOperand(conditionRawOperand))
    return ::mlir::failure();
  {
    auto loc = parser.getCurrentLocation();(void)loc;
    if (parser.parseOptionalAttrDict(result.attributes))
      return ::mlir::failure();
    if (failed(verifyInherentAttrs(result.name, result.attributes, [&]() {
        return parser.emitError(loc) << "'" << result.name.getStringRef() << "' op ";
      })))
      return ::mlir::failure();
  }
  ::mlir::Type odsBuildableType0 = parser.getBuilder().getIntegerType(1);
  if (parser.resolveOperands(conditionOperands, odsBuildableType0, conditionOperandsLoc, result.operands))
    return ::mlir::failure();
  return ::mlir::success();
}
 
void VerifProveOp::print(::mlir::OpAsmPrinter &_odsPrinter) {
  _odsPrinter << ' ';
  _odsPrinter << getCondition();
  ::llvm::SmallVector<::llvm::StringRef, 2> elidedAttrs;
  _odsPrinter.printOptionalAttrDict((*this)->getAttrs(), elidedAttrs);
}
 
// This side effect models "program termination". Based on
// https://github.com/llvm/llvm-project/blob/f325e4b2d836d6e65a4d0cf3efc6b0996ccf3765/mlir/lib/Dialect/ControlFlow/IR/ControlFlowOps.cpp#L92-L97
void VerifProveOp::getEffects(
    ::mlir::SmallVectorImpl<::mlir::SideEffects::EffectInstance<::mlir::MemoryEffects::Effect>> &effects
) {
  effects.emplace_back(::mlir::MemoryEffects::Write::get());
}
 
} // namespace llzk::verif
MLIR_DEFINE_EXPLICIT_TYPE_ID(::llzk::verif::VerifProveOp)
 
namespace llzk::verif {
 
 
//===----------------------------------------------------------------------===//
// ::llzk::verif::VerifSMTProveOp definitions
//===----------------------------------------------------------------------===//
 
namespace detail {
 
VerifSMTProveOpGenericAdaptorBase::VerifSMTProveOpGenericAdaptorBase(VerifSMTProveOp op) : odsAttrs(op->getRawDictionaryAttrs()), odsOpName(op->getName()), properties(op.getProperties()), odsRegions(op->getRegions()) {}
 
 
} // namespace detail
VerifSMTProveOpAdaptor::VerifSMTProveOpAdaptor(VerifSMTProveOp op) : VerifSMTProveOpGenericAdaptor(op->getOperands(), op) {}
 
::llvm::LogicalResult VerifSMTProveOpAdaptor::verify(::mlir::Location loc) {
  return ::mlir::success();
}
 
::llvm::LogicalResult VerifSMTProveOp::setPropertiesFromAttr(Properties &prop, ::mlir::Attribute attr, ::llvm::function_ref<::mlir::InFlightDiagnostic()> emitError) {
  ::mlir::DictionaryAttr dict = ::llvm::dyn_cast<::mlir::DictionaryAttr>(attr);
  if (!dict) {
    emitError() << "expected DictionaryAttr to set properties";
    return ::mlir::failure();
  }
      return ::mlir::success();
}
 
::mlir::Attribute VerifSMTProveOp::getPropertiesAsAttr(::mlir::MLIRContext *ctx, const Properties &prop) {
    ::mlir::SmallVector<::mlir::NamedAttribute> attrs;
    ::mlir::Builder odsBuilder{ctx};
 
  if (!attrs.empty())
    return odsBuilder.getDictionaryAttr(attrs);
  return {};
}
 
llvm::hash_code VerifSMTProveOp::computePropertiesHash(const Properties &prop) {
  using llvm::hash_value;
  return llvm::hash_combine();
}
 
std::optional<mlir::Attribute> VerifSMTProveOp::getInherentAttr(::mlir::MLIRContext *ctx, const Properties &prop, llvm::StringRef name) {
  return std::nullopt;
}
 
void VerifSMTProveOp::setInherentAttr(Properties &prop, llvm::StringRef name, mlir::Attribute value) {
}
 
void VerifSMTProveOp::populateInherentAttrs(::mlir::MLIRContext *ctx, const Properties &prop, ::mlir::NamedAttrList &attrs) {
}
 
::llvm::LogicalResult VerifSMTProveOp::verifyInherentAttrs(::mlir::OperationName opName, ::mlir::NamedAttrList &attrs, llvm::function_ref<::mlir::InFlightDiagnostic()> emitError) {
    return ::mlir::success();
}
 
void VerifSMTProveOp::build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, ::mlir::Value condition) {
  odsState.addOperands(condition);
}
 
VerifSMTProveOp VerifSMTProveOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::Value condition) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(condition)>(condition));
  auto __res__ = ::llvm::dyn_cast<VerifSMTProveOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
VerifSMTProveOp VerifSMTProveOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::Value condition) {
  return create(builder, builder.getLoc(), std::forward<decltype(condition)>(condition));
}
 
void VerifSMTProveOp::build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, ::mlir::TypeRange resultTypes, ::mlir::Value condition) {
  odsState.addOperands(condition);
  assert(resultTypes.size() == 0u && "mismatched number of results");
  odsState.addTypes(resultTypes);
}
 
VerifSMTProveOp VerifSMTProveOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::TypeRange resultTypes, ::mlir::Value condition) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(condition)>(condition));
  auto __res__ = ::llvm::dyn_cast<VerifSMTProveOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
VerifSMTProveOp VerifSMTProveOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::TypeRange resultTypes, ::mlir::Value condition) {
  return create(builder, builder.getLoc(), std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(condition)>(condition));
}
 
void VerifSMTProveOp::build(::mlir::OpBuilder &, ::mlir::OperationState &odsState, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, ::llvm::ArrayRef<::mlir::NamedAttribute> attributes) {
  assert(operands.size() == 1u && "mismatched number of parameters");
  odsState.addOperands(operands);
  odsState.addAttributes(attributes);
  assert(resultTypes.size() == 0u && "mismatched number of return types");
  odsState.addTypes(resultTypes);
}
 
VerifSMTProveOp VerifSMTProveOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, ::llvm::ArrayRef<::mlir::NamedAttribute> attributes) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(operands)>(operands), std::forward<decltype(attributes)>(attributes));
  auto __res__ = ::llvm::dyn_cast<VerifSMTProveOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
VerifSMTProveOp VerifSMTProveOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, ::llvm::ArrayRef<::mlir::NamedAttribute> attributes) {
  return create(builder, builder.getLoc(), std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(operands)>(operands), std::forward<decltype(attributes)>(attributes));
}
 
void VerifSMTProveOp::build(::mlir::OpBuilder &, ::mlir::OperationState &odsState, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, const Properties &properties, ::llvm::ArrayRef<::mlir::NamedAttribute> discardableAttributes) {
  assert(operands.size() == 1u && "mismatched number of parameters");
  odsState.addOperands(operands);
  odsState.useProperties(const_cast<Properties&>(properties));
  odsState.addAttributes(discardableAttributes);
  assert(resultTypes.size() == 0u && "mismatched number of return types");
  odsState.addTypes(resultTypes);
}
 
VerifSMTProveOp VerifSMTProveOp::create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, const Properties &properties, ::llvm::ArrayRef<::mlir::NamedAttribute> discardableAttributes) {
  ::mlir::OperationState __state__(location, getOperationName());
  build(builder, __state__, std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(operands)>(operands), std::forward<decltype(properties)>(properties), std::forward<decltype(discardableAttributes)>(discardableAttributes));
  auto __res__ = ::llvm::dyn_cast<VerifSMTProveOp>(builder.create(__state__));
  assert(__res__ && "builder didn't return the right type");
  return __res__;
}
 
VerifSMTProveOp VerifSMTProveOp::create(::mlir::ImplicitLocOpBuilder &builder, ::mlir::TypeRange resultTypes, ::mlir::ValueRange operands, const Properties &properties, ::llvm::ArrayRef<::mlir::NamedAttribute> discardableAttributes) {
  return create(builder, builder.getLoc(), std::forward<decltype(resultTypes)>(resultTypes), std::forward<decltype(operands)>(operands), std::forward<decltype(properties)>(properties), std::forward<decltype(discardableAttributes)>(discardableAttributes));
}
 
::llvm::LogicalResult VerifSMTProveOp::verifyInvariantsImpl() {
  {
    unsigned index = 0; (void)index;
    auto valueGroup0 = getODSOperands(0);
 
    for (auto v : valueGroup0) {
      if (::mlir::failed(__mlir_ods_local_type_constraint_Ops7(*this, v.getType(), "operand", index++)))
        return ::mlir::failure();
    }
  }
  return ::mlir::success();
}
 
::llvm::LogicalResult VerifSMTProveOp::verifyInvariants() {
  return verifyInvariantsImpl();
}
 
::mlir::ParseResult VerifSMTProveOp::parse(::mlir::OpAsmParser &parser, ::mlir::OperationState &result) {
  ::mlir::OpAsmParser::UnresolvedOperand conditionRawOperand{};
  ::llvm::ArrayRef<::mlir::OpAsmParser::UnresolvedOperand> conditionOperands(&conditionRawOperand, 1);  ::llvm::SMLoc conditionOperandsLoc;
  (void)conditionOperandsLoc;
 
  conditionOperandsLoc = parser.getCurrentLocation();
  if (parser.parseOperand(conditionRawOperand))
    return ::mlir::failure();
  {
    auto loc = parser.getCurrentLocation();(void)loc;
    if (parser.parseOptionalAttrDict(result.attributes))
      return ::mlir::failure();
    if (failed(verifyInherentAttrs(result.name, result.attributes, [&]() {
        return parser.emitError(loc) << "'" << result.name.getStringRef() << "' op ";
      })))
      return ::mlir::failure();
  }
  ::mlir::Type odsBuildableType0 = parser.getBuilder().getType<mlir::smt::BoolType>();
  if (parser.resolveOperands(conditionOperands, odsBuildableType0, conditionOperandsLoc, result.operands))
    return ::mlir::failure();
  return ::mlir::success();
}
 
void VerifSMTProveOp::print(::mlir::OpAsmPrinter &_odsPrinter) {
  _odsPrinter << ' ';
  _odsPrinter << getCondition();
  ::llvm::SmallVector<::llvm::StringRef, 2> elidedAttrs;
  _odsPrinter.printOptionalAttrDict((*this)->getAttrs(), elidedAttrs);
}
 
 
} // namespace llzk::verif
MLIR_DEFINE_EXPLICIT_TYPE_ID(::llzk::verif::VerifSMTProveOp)
 
 
#endif // GET_OP_CLASSES