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
//===----------------------------------------------------------------------===//
 
namespace llzk {
namespace verif {
 
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<::llzk::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 verif
} // namespace llzk
namespace llzk {
namespace verif {
 
//===----------------------------------------------------------------------===//
// ::llzk::verif::AssumeDetOp definitions
//===----------------------------------------------------------------------===//
 
namespace detail {
} // namespace detail
AssumeDetOpAdaptor::AssumeDetOpAdaptor(AssumeDetOp op) : AssumeDetOpGenericAdaptor(op->getOperands(), op) {}
 
::llvm::LogicalResult AssumeDetOpAdaptor::verify(::mlir::Location loc) {
  return ::mlir::success();
}
 
void AssumeDetOp::build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, ::mlir::Value hint) {
  odsState.addOperands(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);
}
 
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);
}
 
::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 (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 verif
} // namespace llzk
MLIR_DEFINE_EXPLICIT_TYPE_ID(::llzk::verif::AssumeDetOp)
 
namespace llzk {
namespace verif {
 
//===----------------------------------------------------------------------===//
// ::llzk::verif::ContractEndOp definitions
//===----------------------------------------------------------------------===//
 
namespace detail {
} // namespace detail
ContractEndOpAdaptor::ContractEndOpAdaptor(ContractEndOp op) : ContractEndOpGenericAdaptor(op->getOperands(), op) {}
 
::llvm::LogicalResult ContractEndOpAdaptor::verify(::mlir::Location loc) {
  return ::mlir::success();
}
 
void ContractEndOp::build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState) {
}
 
void ContractEndOp::build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, ::mlir::TypeRange resultTypes) {
  assert(resultTypes.size() == 0u && "mismatched number of results");
  odsState.addTypes(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);
}
 
::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();
  }
  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 verif
} // namespace llzk
MLIR_DEFINE_EXPLICIT_TYPE_ID(::llzk::verif::ContractEndOp)
 
namespace llzk {
namespace 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);
}
 
} // 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_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");
  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.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.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) {
  return llvm::hash_combine(
    llvm::hash_value(prop.arg_attrs.getAsOpaquePointer()), 
    llvm::hash_value(prop.function_type.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 == "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 == "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.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(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.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.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);
}
 
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) {
        build(odsBuilder, odsState, ::mlir::TypeRange {}, sym_name, target, function_type, arg_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) {
        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;
        }
        initializeEmptyBody(
            odsBuilder, odsState, ::llvm::cast<::mlir::FunctionType>(function_type.getValue())
        );
        assert(resultTypes.size() == 0u && "mismatched number of results");
        odsState.addTypes(resultTypes);
      
}
 
void ContractOp::build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, ::llvm::StringRef sym_name, ::mlir::SymbolRefAttr target, ::mlir::FunctionType function_type, ::mlir::ArrayAttr arg_attrs) {
        build(odsBuilder, odsState, ::mlir::TypeRange {}, sym_name, target, function_type, arg_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) {
        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;
        }
        initializeEmptyBody(odsBuilder, odsState, function_type);
        assert(resultTypes.size() == 0u && "mismatched number of results");
        odsState.addTypes(resultTypes);
      
}
 
::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_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();
  {
    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();
}
 
} // namespace verif
} // namespace llzk
MLIR_DEFINE_EXPLICIT_TYPE_ID(::llzk::verif::ContractOp)
 
namespace llzk {
namespace verif {
 
//===----------------------------------------------------------------------===//
// ::llzk::verif::DecreasesOp definitions
//===----------------------------------------------------------------------===//
 
namespace detail {
} // namespace detail
DecreasesOpAdaptor::DecreasesOpAdaptor(DecreasesOp op) : DecreasesOpGenericAdaptor(op->getOperands(), op) {}
 
::llvm::LogicalResult DecreasesOpAdaptor::verify(::mlir::Location loc) {
  return ::mlir::success();
}
 
void DecreasesOp::build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, ::mlir::Value value) {
  odsState.addOperands(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);
}
 
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);
}
 
::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();
  }
  ::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 verif
} // namespace llzk
MLIR_DEFINE_EXPLICIT_TYPE_ID(::llzk::verif::DecreasesOp)
 
namespace llzk {
namespace verif {
 
//===----------------------------------------------------------------------===//
// ::llzk::verif::EnsureComputeOp definitions
//===----------------------------------------------------------------------===//
 
namespace detail {
} // namespace detail
EnsureComputeOpAdaptor::EnsureComputeOpAdaptor(EnsureComputeOp op) : EnsureComputeOpGenericAdaptor(op->getOperands(), op) {}
 
::llvm::LogicalResult EnsureComputeOpAdaptor::verify(::mlir::Location loc) {
  return ::mlir::success();
}
 
void EnsureComputeOp::build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, ::mlir::Value condition) {
  odsState.addOperands(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);
}
 
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);
}
 
::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();
  }
  ::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 verif
} // namespace llzk
MLIR_DEFINE_EXPLICIT_TYPE_ID(::llzk::verif::EnsureComputeOp)
 
namespace llzk {
namespace verif {
 
//===----------------------------------------------------------------------===//
// ::llzk::verif::EnsureConstrainOp definitions
//===----------------------------------------------------------------------===//
 
namespace detail {
} // namespace detail
EnsureConstrainOpAdaptor::EnsureConstrainOpAdaptor(EnsureConstrainOp op) : EnsureConstrainOpGenericAdaptor(op->getOperands(), op) {}
 
::llvm::LogicalResult EnsureConstrainOpAdaptor::verify(::mlir::Location loc) {
  return ::mlir::success();
}
 
void EnsureConstrainOp::build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, ::mlir::Value condition) {
  odsState.addOperands(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);
}
 
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);
}
 
::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();
  }
  ::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 verif
} // namespace llzk
MLIR_DEFINE_EXPLICIT_TYPE_ID(::llzk::verif::EnsureConstrainOp)
 
namespace llzk {
namespace 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;
}
 
} // namespace detail
IncludeOpAdaptor::IncludeOpAdaptor(IncludeOp op) : IncludeOpGenericAdaptor(op->getOperands(), op) {}
 
::llvm::LogicalResult IncludeOpAdaptor::verify(::mlir::Location loc) {
  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_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");
  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.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.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, emitError)))
        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.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.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 {
    return ::llvm::hash_combine_range(std::begin(propStorage), std::end(propStorage));;
  };
  return llvm::hash_combine(
    llvm::hash_value(prop.callee.getAsOpaquePointer()), 
    llvm::hash_value(prop.mapOpGroupSizes.getAsOpaquePointer()), 
    llvm::hash_value(prop.numDimsPerMap.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 == "callee")
      return prop.callee;
 
    if (name == "mapOpGroupSizes")
      return prop.mapOpGroupSizes;
 
    if (name == "numDimsPerMap")
      return prop.numDimsPerMap;
 
    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 == "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 == "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.callee) attrs.append("callee", prop.callee);
 
    if (prop.mapOpGroupSizes) attrs.append("mapOpGroupSizes", prop.mapOpGroupSizes);
 
    if (prop.numDimsPerMap) attrs.append("numDimsPerMap", prop.numDimsPerMap);
 
    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(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(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.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.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.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.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;
}
 
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);
}
 
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);
                  
}
 
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);
                  
}
 
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);
                  
}
 
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);
                  
}
 
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_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_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();
  {
    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();
  }
  {
 
    auto &propStorage = prop.mapOpGroupSizes;
    auto attr = dict.get("mapOpGroupSizes");
    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();
      }
    }
  }
  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 verif
} // namespace llzk
MLIR_DEFINE_EXPLICIT_TYPE_ID(::llzk::verif::IncludeOp)
 
namespace llzk {
namespace verif {
 
//===----------------------------------------------------------------------===//
// ::llzk::verif::IncreasesOp definitions
//===----------------------------------------------------------------------===//
 
namespace detail {
} // namespace detail
IncreasesOpAdaptor::IncreasesOpAdaptor(IncreasesOp op) : IncreasesOpGenericAdaptor(op->getOperands(), op) {}
 
::llvm::LogicalResult IncreasesOpAdaptor::verify(::mlir::Location loc) {
  return ::mlir::success();
}
 
void IncreasesOp::build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, ::mlir::Value value) {
  odsState.addOperands(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);
}
 
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);
}
 
::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();
  }
  ::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 verif
} // namespace llzk
MLIR_DEFINE_EXPLICIT_TYPE_ID(::llzk::verif::IncreasesOp)
 
namespace llzk {
namespace 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) {
  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);
}
 
::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();
}
 
} // namespace verif
} // namespace llzk
MLIR_DEFINE_EXPLICIT_TYPE_ID(::llzk::verif::InvariantOp)
 
namespace llzk {
namespace verif {
 
//===----------------------------------------------------------------------===//
// ::llzk::verif::OldOp definitions
//===----------------------------------------------------------------------===//
 
namespace detail {
} // namespace detail
OldOpAdaptor::OldOpAdaptor(OldOp op) : OldOpGenericAdaptor(op->getOperands(), op) {}
 
::llvm::LogicalResult OldOpAdaptor::verify(::mlir::Location loc) {
  return ::mlir::success();
}
 
void OldOp::build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, ::mlir::Type result, ::mlir::Value value) {
  odsState.addOperands(value);
  odsState.addTypes(result);
}
 
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);
        
}
 
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);
}
 
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);
}
 
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).");
  }
}
 
::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::OpaqueProperties 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();
  }
  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 verif
} // namespace llzk
MLIR_DEFINE_EXPLICIT_TYPE_ID(::llzk::verif::OldOp)
 
namespace llzk {
namespace verif {
 
//===----------------------------------------------------------------------===//
// ::llzk::verif::ProveDetOp definitions
//===----------------------------------------------------------------------===//
 
namespace detail {
} // namespace detail
ProveDetOpAdaptor::ProveDetOpAdaptor(ProveDetOp op) : ProveDetOpGenericAdaptor(op->getOperands(), op) {}
 
::llvm::LogicalResult ProveDetOpAdaptor::verify(::mlir::Location loc) {
  return ::mlir::success();
}
 
void ProveDetOp::build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, ::mlir::Type result, ::mlir::Value condition) {
  odsState.addOperands(condition);
  odsState.addTypes(result);
}
 
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);
        
}
 
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);
}
 
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);
}
 
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).");
  }
}
 
::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::OpaqueProperties 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 (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 verif
} // namespace llzk
MLIR_DEFINE_EXPLICIT_TYPE_ID(::llzk::verif::ProveDetOp)
 
namespace llzk {
namespace verif {
 
//===----------------------------------------------------------------------===//
// ::llzk::verif::RequireComputeOp definitions
//===----------------------------------------------------------------------===//
 
namespace detail {
} // namespace detail
RequireComputeOpAdaptor::RequireComputeOpAdaptor(RequireComputeOp op) : RequireComputeOpGenericAdaptor(op->getOperands(), op) {}
 
::llvm::LogicalResult RequireComputeOpAdaptor::verify(::mlir::Location loc) {
  return ::mlir::success();
}
 
void RequireComputeOp::build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, ::mlir::Value condition) {
  odsState.addOperands(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);
}
 
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);
}
 
::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();
  }
  ::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 verif
} // namespace llzk
MLIR_DEFINE_EXPLICIT_TYPE_ID(::llzk::verif::RequireComputeOp)
 
namespace llzk {
namespace verif {
 
//===----------------------------------------------------------------------===//
// ::llzk::verif::RequireConstrainOp definitions
//===----------------------------------------------------------------------===//
 
namespace detail {
} // namespace detail
RequireConstrainOpAdaptor::RequireConstrainOpAdaptor(RequireConstrainOp op) : RequireConstrainOpGenericAdaptor(op->getOperands(), op) {}
 
::llvm::LogicalResult RequireConstrainOpAdaptor::verify(::mlir::Location loc) {
  return ::mlir::success();
}
 
void RequireConstrainOp::build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, ::mlir::Value condition) {
  odsState.addOperands(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);
}
 
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);
}
 
::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();
  }
  ::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 verif
} // namespace llzk
MLIR_DEFINE_EXPLICIT_TYPE_ID(::llzk::verif::RequireConstrainOp)
 
namespace llzk {
namespace verif {
 
//===----------------------------------------------------------------------===//
// ::llzk::verif::StepOp definitions
//===----------------------------------------------------------------------===//
 
namespace detail {
} // namespace detail
StepOpAdaptor::StepOpAdaptor(StepOp op) : StepOpGenericAdaptor(op->getOperands(), op) {}
 
::llvm::LogicalResult StepOpAdaptor::verify(::mlir::Location loc) {
  return ::mlir::success();
}
 
void StepOp::build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState) {
  (void)odsState.addRegion();
}
 
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);
}
 
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);
}
 
::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();
  }
  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 verif
} // namespace llzk
MLIR_DEFINE_EXPLICIT_TYPE_ID(::llzk::verif::StepOp)
 
namespace llzk {
namespace verif {
 
//===----------------------------------------------------------------------===//
// ::llzk::verif::StepYieldOp definitions
//===----------------------------------------------------------------------===//
 
namespace detail {
} // namespace detail
StepYieldOpAdaptor::StepYieldOpAdaptor(StepYieldOp op) : StepYieldOpGenericAdaptor(op->getOperands(), op) {}
 
::llvm::LogicalResult StepYieldOpAdaptor::verify(::mlir::Location loc) {
  return ::mlir::success();
}
 
void StepYieldOp::build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, ::mlir::Value value) {
  odsState.addOperands(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);
}
 
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);
}
 
::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();
  }
  ::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 verif
} // namespace llzk
MLIR_DEFINE_EXPLICIT_TYPE_ID(::llzk::verif::StepYieldOp)
 
namespace llzk {
namespace verif {
 
//===----------------------------------------------------------------------===//
// ::llzk::verif::VerifAssertOp definitions
//===----------------------------------------------------------------------===//
 
namespace detail {
} // namespace detail
VerifAssertOpAdaptor::VerifAssertOpAdaptor(VerifAssertOp op) : VerifAssertOpGenericAdaptor(op->getOperands(), op) {}
 
::llvm::LogicalResult VerifAssertOpAdaptor::verify(::mlir::Location loc) {
  return ::mlir::success();
}
 
void VerifAssertOp::build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, ::mlir::Value condition) {
  odsState.addOperands(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);
}
 
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);
}
 
::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();
  }
  ::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 verif
} // namespace llzk
MLIR_DEFINE_EXPLICIT_TYPE_ID(::llzk::verif::VerifAssertOp)
 
namespace llzk {
namespace verif {
 
//===----------------------------------------------------------------------===//
// ::llzk::verif::VerifProveOp definitions
//===----------------------------------------------------------------------===//
 
namespace detail {
} // namespace detail
VerifProveOpAdaptor::VerifProveOpAdaptor(VerifProveOp op) : VerifProveOpGenericAdaptor(op->getOperands(), op) {}
 
::llvm::LogicalResult VerifProveOpAdaptor::verify(::mlir::Location loc) {
  return ::mlir::success();
}
 
void VerifProveOp::build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, ::mlir::Value condition) {
  odsState.addOperands(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);
}
 
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);
}
 
::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();
  }
  ::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 verif
} // namespace llzk
MLIR_DEFINE_EXPLICIT_TYPE_ID(::llzk::verif::VerifProveOp)
 
namespace llzk {
namespace verif {
 
//===----------------------------------------------------------------------===//
// ::llzk::verif::VerifSMTProveOp definitions
//===----------------------------------------------------------------------===//
 
namespace detail {
} // namespace detail
VerifSMTProveOpAdaptor::VerifSMTProveOpAdaptor(VerifSMTProveOp op) : VerifSMTProveOpGenericAdaptor(op->getOperands(), op) {}
 
::llvm::LogicalResult VerifSMTProveOpAdaptor::verify(::mlir::Location loc) {
  return ::mlir::success();
}
 
void VerifSMTProveOp::build(::mlir::OpBuilder &odsBuilder, ::mlir::OperationState &odsState, ::mlir::Value condition) {
  odsState.addOperands(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);
}
 
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);
}
 
::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();
  }
  ::mlir::Type odsBuildableType0 = parser.getBuilder().getType<::llzk::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 verif
} // namespace llzk
MLIR_DEFINE_EXPLICIT_TYPE_ID(::llzk::verif::VerifSMTProveOp)
 
 
#endif  // GET_OP_CLASSES