17 MlirOperationState state = mlirOperationStateGet(mlirStringRefCreateFromCString(
"verif.contract_end"), location);
23 return llvm::isa<ContractEndOp>(unwrap(inp));
27 return llvm::isa<ContractOp>(unwrap(inp));
31 return mlirOperationGetAttributeByName(op, mlirStringRefCreateFromCString(
"sym_name"));
35 mlirOperationSetAttributeByName(op, mlirStringRefCreateFromCString(
"sym_name"), attr);
39 return mlirOperationGetAttributeByName(op, mlirStringRefCreateFromCString(
"target"));
43 mlirOperationSetAttributeByName(op, mlirStringRefCreateFromCString(
"target"), attr);
47 return mlirOperationGetAttributeByName(op, mlirStringRefCreateFromCString(
"function_type"));
51 mlirOperationSetAttributeByName(op, mlirStringRefCreateFromCString(
"function_type"), attr);
55 return mlirOperationGetAttributeByName(op, mlirStringRefCreateFromCString(
"arg_attrs"));
59 mlirOperationSetAttributeByName(op, mlirStringRefCreateFromCString(
"arg_attrs"), attr);
63 return mlirOperationGetRegion(op, 0);
67 return llvm::cast<ContractOp>(unwrap(inp)).isDeclaration();
71 return llvm::cast<ContractOp>(unwrap(inp)).hasArgPublicAttr(index);
75 return llvm::cast<ContractOp>(unwrap(inp)).hasFuncTarget();
79 return llvm::cast<ContractOp>(unwrap(inp)).hasStructTarget();
83 return wrap(llvm::cast<ContractOp>(unwrap(inp)).getCallableRegion());
87 return llvm::cast<ContractOp>(unwrap(inp)).hasArgName(index);
91 return wrap(llvm::cast<ContractOp>(unwrap(inp)).getFullyQualifiedName(requireParent));
95 MlirOperationState state = mlirOperationStateGet(mlirStringRefCreateFromCString(
"verif.decreases"), location);
96 mlirOperationStateAddOperands(&state, 1, &value);
102 return llvm::isa<DecreasesOp>(unwrap(inp));
106 auto range = llvm::cast<DecreasesOp>(unwrap(op)).getODSOperandIndexAndLength(0);
107 assert(range.second == 1 &&
"expected fixed operand segment size");
109 static_cast<uintptr_t
>(range.first) <=
static_cast<uintptr_t
>(std::numeric_limits<intptr_t>::max()) &&
110 "operand index exceeds intptr_t range"
112 return mlirOperationGetOperand(op,
static_cast<intptr_t
>(range.first));
116 auto range = llvm::cast<DecreasesOp>(unwrap(op)).getODSOperandIndexAndLength(0);
117 assert(range.second == 1 &&
"expected fixed operand segment size");
119 static_cast<uintptr_t
>(range.first) <=
static_cast<uintptr_t
>(std::numeric_limits<intptr_t>::max()) &&
120 "operand index exceeds intptr_t range"
122 mlirOperationSetOperand(op,
static_cast<intptr_t
>(range.first), value);
126 MlirOperationState state = mlirOperationStateGet(mlirStringRefCreateFromCString(
"verif.ensure_compute"), location);
127 mlirOperationStateAddOperands(&state, 1, &condition);
133 return llvm::isa<EnsureComputeOp>(unwrap(inp));
137 auto range = llvm::cast<EnsureComputeOp>(unwrap(op)).getODSOperandIndexAndLength(0);
138 assert(range.second == 1 &&
"expected fixed operand segment size");
140 static_cast<uintptr_t
>(range.first) <=
static_cast<uintptr_t
>(std::numeric_limits<intptr_t>::max()) &&
141 "operand index exceeds intptr_t range"
143 return mlirOperationGetOperand(op,
static_cast<intptr_t
>(range.first));
147 auto range = llvm::cast<EnsureComputeOp>(unwrap(op)).getODSOperandIndexAndLength(0);
148 assert(range.second == 1 &&
"expected fixed operand segment size");
150 static_cast<uintptr_t
>(range.first) <=
static_cast<uintptr_t
>(std::numeric_limits<intptr_t>::max()) &&
151 "operand index exceeds intptr_t range"
153 mlirOperationSetOperand(op,
static_cast<intptr_t
>(range.first), value);
157 MlirOperationState state = mlirOperationStateGet(mlirStringRefCreateFromCString(
"verif.ensure_constrain"), location);
158 mlirOperationStateAddOperands(&state, 1, &condition);
164 return llvm::isa<EnsureConstrainOp>(unwrap(inp));
168 auto range = llvm::cast<EnsureConstrainOp>(unwrap(op)).getODSOperandIndexAndLength(0);
169 assert(range.second == 1 &&
"expected fixed operand segment size");
171 static_cast<uintptr_t
>(range.first) <=
static_cast<uintptr_t
>(std::numeric_limits<intptr_t>::max()) &&
172 "operand index exceeds intptr_t range"
174 return mlirOperationGetOperand(op,
static_cast<intptr_t
>(range.first));
178 auto range = llvm::cast<EnsureConstrainOp>(unwrap(op)).getODSOperandIndexAndLength(0);
179 assert(range.second == 1 &&
"expected fixed operand segment size");
181 static_cast<uintptr_t
>(range.first) <=
static_cast<uintptr_t
>(std::numeric_limits<intptr_t>::max()) &&
182 "operand index exceeds intptr_t range"
184 mlirOperationSetOperand(op,
static_cast<intptr_t
>(range.first), value);
188 return llvm::isa<IncludeOp>(unwrap(inp));
192 auto range = llvm::cast<IncludeOp>(unwrap(op)).getODSOperandIndexAndLength(0);
197 auto range = llvm::cast<IncludeOp>(unwrap(op)).getODSOperandIndexAndLength(0);
198 assert(index >= 0 && index < range.second &&
"variadic operand index out of range");
200 static_cast<uintptr_t
>(range.first) <=
static_cast<uintptr_t
>(std::numeric_limits<intptr_t>::max()) &&
201 "operand index exceeds intptr_t range"
203 return mlirOperationGetOperand(op,
static_cast<intptr_t
>(range.first) + index);
209 ::llvm::SmallVector<::mlir::Value> vals;
210 vals.reserve(
static_cast<size_t>(count));
211 for (intptr_t i = 0; i < count; ++i)
212 vals.push_back(unwrap(values[i]));
213 ::llvm::cast<IncludeOp>(unwrap(op)).getArgOperandsMutable().assign(vals);
217 auto range = llvm::cast<IncludeOp>(unwrap(op)).getODSOperandIndexAndLength(1);
222 auto range = llvm::cast<IncludeOp>(unwrap(op)).getODSOperandIndexAndLength(1);
223 assert(index >= 0 && index < range.second &&
"variadic operand index out of range");
225 static_cast<uintptr_t
>(range.first) <=
static_cast<uintptr_t
>(std::numeric_limits<intptr_t>::max()) &&
226 "operand index exceeds intptr_t range"
228 return mlirOperationGetOperand(op,
static_cast<intptr_t
>(range.first) + index);
235 ::llvm::SmallVector<::mlir::Value> vals;
236 for (intptr_t g = 0; g < groupCount; ++g) {
237 assert(groups[g].size >= 0 &&
"group size must be non-negative");
238 for (intptr_t i = 0; i < groups[g].
size; ++i) {
239 vals.push_back(unwrap(groups[g].values[i]));
242 ::llvm::cast<IncludeOp>(unwrap(op)).getMapOperandsMutable().join().assign(vals);
244 ::llvm::SmallVector<int32_t> newGroupSizes;
245 newGroupSizes.reserve(
static_cast<size_t>(groupCount));
246 for (intptr_t g = 0; g < groupCount; ++g) {
248 groups[g].size <=
static_cast<intptr_t
>(std::numeric_limits<int32_t>::max()) &&
249 "group size exceeds int32_t range"
251 newGroupSizes.push_back(
static_cast<int32_t
>(groups[g].size));
253 MlirContext ctx = mlirOperationGetContext(op);
255 newGroupSizes.size() <=
static_cast<size_t>(std::numeric_limits<intptr_t>::max()) &&
256 "group count exceeds intptr_t range"
258 mlirOperationSetAttributeByName(
259 op, mlirStringRefCreateFromCString(
"mapOpGroupSizes"),
260 mlirDenseI32ArrayGet(ctx,
static_cast<intptr_t
>(newGroupSizes.size()), newGroupSizes.data())
265 return mlirOperationGetAttributeByName(op, mlirStringRefCreateFromCString(
"callee"));
269 mlirOperationSetAttributeByName(op, mlirStringRefCreateFromCString(
"callee"), attr);
273 return mlirOperationGetAttributeByName(op, mlirStringRefCreateFromCString(
"templateParams"));
277 mlirOperationSetAttributeByName(op, mlirStringRefCreateFromCString(
"templateParams"), attr);
281 return mlirOperationGetAttributeByName(op, mlirStringRefCreateFromCString(
"numDimsPerMap"));
285 mlirOperationSetAttributeByName(op, mlirStringRefCreateFromCString(
"numDimsPerMap"), attr);
289 return mlirOperationGetAttributeByName(op, mlirStringRefCreateFromCString(
"mapOpGroupSizes"));
293 mlirOperationSetAttributeByName(op, mlirStringRefCreateFromCString(
"mapOpGroupSizes"), attr);
297 return llvm::cast<IncludeOp>(unwrap(inp)).contractTargetsStruct();
301 return wrap(llvm::cast<IncludeOp>(unwrap(inp)).getSelfValue());
305 return wrap(llvm::cast<IncludeOp>(unwrap(inp)).getTypeSignature());
309 return wrap(llvm::cast<IncludeOp>(unwrap(inp)).resolveCallable());
313 MlirOperationState state = mlirOperationStateGet(mlirStringRefCreateFromCString(
"verif.increases"), location);
314 mlirOperationStateAddOperands(&state, 1, &value);
320 return llvm::isa<IncreasesOp>(unwrap(inp));
324 auto range = llvm::cast<IncreasesOp>(unwrap(op)).getODSOperandIndexAndLength(0);
325 assert(range.second == 1 &&
"expected fixed operand segment size");
327 static_cast<uintptr_t
>(range.first) <=
static_cast<uintptr_t
>(std::numeric_limits<intptr_t>::max()) &&
328 "operand index exceeds intptr_t range"
330 return mlirOperationGetOperand(op,
static_cast<intptr_t
>(range.first));
334 auto range = llvm::cast<IncreasesOp>(unwrap(op)).getODSOperandIndexAndLength(0);
335 assert(range.second == 1 &&
"expected fixed operand segment size");
337 static_cast<uintptr_t
>(range.first) <=
static_cast<uintptr_t
>(std::numeric_limits<intptr_t>::max()) &&
338 "operand index exceeds intptr_t range"
340 mlirOperationSetOperand(op,
static_cast<intptr_t
>(range.first), value);
344 return llvm::isa<InvariantOp>(unwrap(inp));
348 return mlirOperationGetAttributeByName(op, mlirStringRefCreateFromCString(
"loop_name"));
352 mlirOperationSetAttributeByName(op, mlirStringRefCreateFromCString(
"loop_name"), attr);
356 return mlirOperationGetAttributeByName(op, mlirStringRefCreateFromCString(
"loop_arg_types"));
360 mlirOperationSetAttributeByName(op, mlirStringRefCreateFromCString(
"loop_arg_types"), attr);
364 return mlirOperationGetRegion(op, 0);
368 return wrap(llvm::cast<InvariantOp>(unwrap(inp)).getParentContract());
372 MlirOperationState state = mlirOperationStateGet(mlirStringRefCreateFromCString(
"verif.old"), location);
373 mlirOperationStateEnableResultTypeInference(&state);
374 mlirOperationStateAddOperands(&state, 1, &value);
380 return llvm::isa<OldOp>(unwrap(inp));
384 auto range = llvm::cast<OldOp>(unwrap(op)).getODSOperandIndexAndLength(0);
385 assert(range.second == 1 &&
"expected fixed operand segment size");
387 static_cast<uintptr_t
>(range.first) <=
static_cast<uintptr_t
>(std::numeric_limits<intptr_t>::max()) &&
388 "operand index exceeds intptr_t range"
390 return mlirOperationGetOperand(op,
static_cast<intptr_t
>(range.first));
394 auto range = llvm::cast<OldOp>(unwrap(op)).getODSOperandIndexAndLength(0);
395 assert(range.second == 1 &&
"expected fixed operand segment size");
397 static_cast<uintptr_t
>(range.first) <=
static_cast<uintptr_t
>(std::numeric_limits<intptr_t>::max()) &&
398 "operand index exceeds intptr_t range"
400 mlirOperationSetOperand(op,
static_cast<intptr_t
>(range.first), value);
404 return mlirOperationGetResult(op, 0);
408 MlirOperationState state = mlirOperationStateGet(mlirStringRefCreateFromCString(
"verif.require_compute"), location);
409 mlirOperationStateAddOperands(&state, 1, &condition);
415 return llvm::isa<RequireComputeOp>(unwrap(inp));
419 auto range = llvm::cast<RequireComputeOp>(unwrap(op)).getODSOperandIndexAndLength(0);
420 assert(range.second == 1 &&
"expected fixed operand segment size");
422 static_cast<uintptr_t
>(range.first) <=
static_cast<uintptr_t
>(std::numeric_limits<intptr_t>::max()) &&
423 "operand index exceeds intptr_t range"
425 return mlirOperationGetOperand(op,
static_cast<intptr_t
>(range.first));
429 auto range = llvm::cast<RequireComputeOp>(unwrap(op)).getODSOperandIndexAndLength(0);
430 assert(range.second == 1 &&
"expected fixed operand segment size");
432 static_cast<uintptr_t
>(range.first) <=
static_cast<uintptr_t
>(std::numeric_limits<intptr_t>::max()) &&
433 "operand index exceeds intptr_t range"
435 mlirOperationSetOperand(op,
static_cast<intptr_t
>(range.first), value);
439 MlirOperationState state = mlirOperationStateGet(mlirStringRefCreateFromCString(
"verif.require_constrain"), location);
440 mlirOperationStateAddOperands(&state, 1, &condition);
446 return llvm::isa<RequireConstrainOp>(unwrap(inp));
450 auto range = llvm::cast<RequireConstrainOp>(unwrap(op)).getODSOperandIndexAndLength(0);
451 assert(range.second == 1 &&
"expected fixed operand segment size");
453 static_cast<uintptr_t
>(range.first) <=
static_cast<uintptr_t
>(std::numeric_limits<intptr_t>::max()) &&
454 "operand index exceeds intptr_t range"
456 return mlirOperationGetOperand(op,
static_cast<intptr_t
>(range.first));
460 auto range = llvm::cast<RequireConstrainOp>(unwrap(op)).getODSOperandIndexAndLength(0);
461 assert(range.second == 1 &&
"expected fixed operand segment size");
463 static_cast<uintptr_t
>(range.first) <=
static_cast<uintptr_t
>(std::numeric_limits<intptr_t>::max()) &&
464 "operand index exceeds intptr_t range"
466 mlirOperationSetOperand(op,
static_cast<intptr_t
>(range.first), value);
470 MlirOperationState state = mlirOperationStateGet(mlirStringRefCreateFromCString(
"verif.step"), location);
471 llvm::SmallVector<MlirRegion, 1> regions;
472 regions.push_back(mlirRegionCreate());
473 mlirOperationStateAddOwnedRegions(&state, regions.size(), regions.data());
479 return llvm::isa<StepOp>(unwrap(inp));
483 return mlirOperationGetRegion(op, 0);
487 MlirOperationState state = mlirOperationStateGet(mlirStringRefCreateFromCString(
"verif.step.yield"), location);
488 mlirOperationStateAddOperands(&state, 1, &value);
494 return llvm::isa<StepYieldOp>(unwrap(inp));
498 auto range = llvm::cast<StepYieldOp>(unwrap(op)).getODSOperandIndexAndLength(0);
499 assert(range.second == 1 &&
"expected fixed operand segment size");
501 static_cast<uintptr_t
>(range.first) <=
static_cast<uintptr_t
>(std::numeric_limits<intptr_t>::max()) &&
502 "operand index exceeds intptr_t range"
504 return mlirOperationGetOperand(op,
static_cast<intptr_t
>(range.first));
508 auto range = llvm::cast<StepYieldOp>(unwrap(op)).getODSOperandIndexAndLength(0);
509 assert(range.second == 1 &&
"expected fixed operand segment size");
511 static_cast<uintptr_t
>(range.first) <=
static_cast<uintptr_t
>(std::numeric_limits<intptr_t>::max()) &&
512 "operand index exceeds intptr_t range"
514 mlirOperationSetOperand(op,
static_cast<intptr_t
>(range.first), value);
518 MlirOperationState state = mlirOperationStateGet(mlirStringRefCreateFromCString(
"verif.assert"), location);
519 mlirOperationStateAddOperands(&state, 1, &condition);
525 return llvm::isa<VerifAssertOp>(unwrap(inp));
529 auto range = llvm::cast<VerifAssertOp>(unwrap(op)).getODSOperandIndexAndLength(0);
530 assert(range.second == 1 &&
"expected fixed operand segment size");
532 static_cast<uintptr_t
>(range.first) <=
static_cast<uintptr_t
>(std::numeric_limits<intptr_t>::max()) &&
533 "operand index exceeds intptr_t range"
535 return mlirOperationGetOperand(op,
static_cast<intptr_t
>(range.first));
539 auto range = llvm::cast<VerifAssertOp>(unwrap(op)).getODSOperandIndexAndLength(0);
540 assert(range.second == 1 &&
"expected fixed operand segment size");
542 static_cast<uintptr_t
>(range.first) <=
static_cast<uintptr_t
>(std::numeric_limits<intptr_t>::max()) &&
543 "operand index exceeds intptr_t range"
545 mlirOperationSetOperand(op,
static_cast<intptr_t
>(range.first), value);
549 MlirOperationState state = mlirOperationStateGet(mlirStringRefCreateFromCString(
"verif.prove"), location);
550 mlirOperationStateAddOperands(&state, 1, &condition);
556 return llvm::isa<VerifProveOp>(unwrap(inp));
560 auto range = llvm::cast<VerifProveOp>(unwrap(op)).getODSOperandIndexAndLength(0);
561 assert(range.second == 1 &&
"expected fixed operand segment size");
563 static_cast<uintptr_t
>(range.first) <=
static_cast<uintptr_t
>(std::numeric_limits<intptr_t>::max()) &&
564 "operand index exceeds intptr_t range"
566 return mlirOperationGetOperand(op,
static_cast<intptr_t
>(range.first));
570 auto range = llvm::cast<VerifProveOp>(unwrap(op)).getODSOperandIndexAndLength(0);
571 assert(range.second == 1 &&
"expected fixed operand segment size");
573 static_cast<uintptr_t
>(range.first) <=
static_cast<uintptr_t
>(std::numeric_limits<intptr_t>::max()) &&
574 "operand index exceeds intptr_t range"
576 mlirOperationSetOperand(op,
static_cast<intptr_t
>(range.first), value);
580 MlirOperationState state = mlirOperationStateGet(mlirStringRefCreateFromCString(
"verif.smt_prove"), location);
581 mlirOperationStateAddOperands(&state, 1, &condition);
587 return llvm::isa<VerifSMTProveOp>(unwrap(inp));
591 auto range = llvm::cast<VerifSMTProveOp>(unwrap(op)).getODSOperandIndexAndLength(0);
592 assert(range.second == 1 &&
"expected fixed operand segment size");
594 static_cast<uintptr_t
>(range.first) <=
static_cast<uintptr_t
>(std::numeric_limits<intptr_t>::max()) &&
595 "operand index exceeds intptr_t range"
597 return mlirOperationGetOperand(op,
static_cast<intptr_t
>(range.first));
601 auto range = llvm::cast<VerifSMTProveOp>(unwrap(op)).getODSOperandIndexAndLength(0);
602 assert(range.second == 1 &&
"expected fixed operand segment size");
604 static_cast<uintptr_t
>(range.first) <=
static_cast<uintptr_t
>(std::numeric_limits<intptr_t>::max()) &&
605 "operand index exceeds intptr_t range"
607 mlirOperationSetOperand(op,
static_cast<intptr_t
>(range.first), value);
MlirOperation mlirOpBuilderInsert(MlirOpBuilder builder, MlirOperation op)
Inserts op at the current insertion point of builder and returns it.
MlirValue llzkVerif_OldOpGetValue(MlirOperation op)
Get Value operand from llzk::verif::OldOp Operation.
MlirAttribute llzkVerif_IncludeOpGetNumDimsPerMap(MlirOperation op)
Get NumDimsPerMap attribute from llzk::verif::IncludeOp Operation.
intptr_t llzkVerif_IncludeOpGetMapOperandsCount(MlirOperation op)
Get number of MapOperands operands in llzk::verif::IncludeOp Operation.
void llzkVerif_StepYieldOpSetValue(MlirOperation op, MlirValue value)
Set Value operand of llzk::verif::StepYieldOp Operation.
void llzkVerif_VerifAssertOpSetCondition(MlirOperation op, MlirValue value)
Set Condition operand of llzk::verif::VerifAssertOp Operation.
void llzkVerif_IncludeOpSetTemplateParams(MlirOperation op, MlirAttribute attr)
Set TemplateParams attribute of llzk::verif::IncludeOp Operation.
void llzkVerif_IncludeOpSetMapOpGroupSizes(MlirOperation op, MlirAttribute attr)
Set MapOpGroupSizes attribute of llzk::verif::IncludeOp Operation.
MlirValue llzkVerif_VerifProveOpGetCondition(MlirOperation op)
Get Condition operand from llzk::verif::VerifProveOp Operation.
void llzkVerif_VerifProveOpSetCondition(MlirOperation op, MlirValue value)
Set Condition operand of llzk::verif::VerifProveOp Operation.
MlirOperation llzkVerif_RequireComputeOpBuild(MlirOpBuilder builder, MlirLocation location, MlirValue condition)
Build a llzk::verif::RequireComputeOp Operation.
void llzkVerif_IncludeOpSetCallee(MlirOperation op, MlirAttribute attr)
Set Callee attribute of llzk::verif::IncludeOp Operation.
MlirOperation llzkVerif_RequireConstrainOpBuild(MlirOpBuilder builder, MlirLocation location, MlirValue condition)
Build a llzk::verif::RequireConstrainOp Operation.
bool llzkVerif_ContractOpHasStructTarget(MlirOperation inp)
Return true iff the contract targets a struct type.
void llzkVerif_RequireConstrainOpSetCondition(MlirOperation op, MlirValue value)
Set Condition operand of llzk::verif::RequireConstrainOp Operation.
MlirValue llzkVerif_VerifSMTProveOpGetCondition(MlirOperation op)
Get Condition operand from llzk::verif::VerifSMTProveOp Operation.
MlirRegion llzkVerif_ContractOpGetBody(MlirOperation op)
Get Body region from llzk::verif::ContractOp Operation.
MlirAttribute llzkVerif_IncludeOpGetTemplateParams(MlirOperation op)
Get TemplateParams attribute from llzk::verif::IncludeOp Operation.
MlirOperation llzkVerif_StepOpBuild(MlirOpBuilder builder, MlirLocation location)
Build a llzk::verif::StepOp Operation.
bool llzkOperationIsA_Verif_RequireConstrainOp(MlirOperation inp)
Returns true if the Operation is a llzk::verif::RequireConstrainOp.
MlirOperation llzkVerif_EnsureConstrainOpBuild(MlirOpBuilder builder, MlirLocation location, MlirValue condition)
Build a llzk::verif::EnsureConstrainOp Operation.
MlirAttribute llzkVerif_IncludeOpGetMapOpGroupSizes(MlirOperation op)
Get MapOpGroupSizes attribute from llzk::verif::IncludeOp Operation.
bool llzkOperationIsA_Verif_VerifSMTProveOp(MlirOperation inp)
Returns true if the Operation is a llzk::verif::VerifSMTProveOp.
MlirOperation llzkVerif_ContractEndOpBuild(MlirOpBuilder builder, MlirLocation location)
Build a llzk::verif::ContractEndOp Operation.
void llzkVerif_EnsureComputeOpSetCondition(MlirOperation op, MlirValue value)
Set Condition operand of llzk::verif::EnsureComputeOp Operation.
MlirValue llzkVerif_StepYieldOpGetValue(MlirOperation op)
Get Value operand from llzk::verif::StepYieldOp Operation.
MlirOperation llzkVerif_VerifProveOpBuild(MlirOpBuilder builder, MlirLocation location, MlirValue condition)
Build a llzk::verif::VerifProveOp Operation.
MlirOperation llzkVerif_VerifSMTProveOpBuild(MlirOpBuilder builder, MlirLocation location, MlirValue condition)
Build a llzk::verif::VerifSMTProveOp Operation.
MlirAttribute llzkVerif_InvariantOpGetLoopName(MlirOperation op)
Get LoopName attribute from llzk::verif::InvariantOp Operation.
bool llzkVerif_ContractOpHasArgPublicAttr(MlirOperation inp, unsigned index)
Return true iff the argument at the given index has pub attribute.
bool llzkOperationIsA_Verif_ContractEndOp(MlirOperation inp)
Returns true if the Operation is a llzk::verif::ContractEndOp.
MlirRegion llzkVerif_StepOpGetRegion(MlirOperation op)
Get Region region from llzk::verif::StepOp Operation.
intptr_t llzkVerif_IncludeOpGetArgOperandsCount(MlirOperation op)
Get number of ArgOperands operands in llzk::verif::IncludeOp Operation.
bool llzkOperationIsA_Verif_DecreasesOp(MlirOperation inp)
Returns true if the Operation is a llzk::verif::DecreasesOp.
bool llzkOperationIsA_Verif_StepYieldOp(MlirOperation inp)
Returns true if the Operation is a llzk::verif::StepYieldOp.
bool llzkOperationIsA_Verif_InvariantOp(MlirOperation inp)
Returns true if the Operation is a llzk::verif::InvariantOp.
MlirAttribute llzkVerif_ContractOpGetSymName(MlirOperation op)
Get SymName attribute from llzk::verif::ContractOp Operation.
void llzkVerif_IncreasesOpSetValue(MlirOperation op, MlirValue value)
Set Value operand of llzk::verif::IncreasesOp Operation.
MlirValue llzkVerif_VerifAssertOpGetCondition(MlirOperation op)
Get Condition operand from llzk::verif::VerifAssertOp Operation.
MlirOperation llzkVerif_IncreasesOpBuild(MlirOpBuilder builder, MlirLocation location, MlirValue value)
Build a llzk::verif::IncreasesOp Operation.
MlirAttribute llzkVerif_InvariantOpGetLoopArgTypes(MlirOperation op)
Get LoopArgTypes attribute from llzk::verif::InvariantOp Operation.
MlirOperation llzkVerif_OldOpBuild(MlirOpBuilder builder, MlirLocation location, MlirValue value)
Build a llzk::verif::OldOp Operation.
void llzkVerif_VerifSMTProveOpSetCondition(MlirOperation op, MlirValue value)
Set Condition operand of llzk::verif::VerifSMTProveOp Operation.
bool llzkVerif_ContractOpHasArgName(MlirOperation inp, unsigned index)
Return true iff the argument at the given index has a function.arg_name attribute.
bool llzkVerif_IncludeOpContractTargetsStruct(MlirOperation inp)
Return true iff the contract targets a struct type.
bool llzkOperationIsA_Verif_RequireComputeOp(MlirOperation inp)
Returns true if the Operation is a llzk::verif::RequireComputeOp.
MlirAttribute llzkVerif_ContractOpGetTarget(MlirOperation op)
Get Target attribute from llzk::verif::ContractOp Operation.
MlirAttribute llzkVerif_ContractOpGetFunctionType(MlirOperation op)
Get FunctionType attribute from llzk::verif::ContractOp Operation.
bool llzkOperationIsA_Verif_EnsureConstrainOp(MlirOperation inp)
Returns true if the Operation is a llzk::verif::EnsureConstrainOp.
MlirAttribute llzkVerif_ContractOpGetArgAttrs(MlirOperation op)
Get ArgAttrs attribute from llzk::verif::ContractOp Operation.
bool llzkOperationIsA_Verif_EnsureComputeOp(MlirOperation inp)
Returns true if the Operation is a llzk::verif::EnsureComputeOp.
void llzkVerif_IncludeOpSetArgOperands(MlirOperation op, intptr_t count, MlirValue const *values)
Set ArgOperands operands of llzk::verif::IncludeOp Operation.
MlirOperation llzkVerif_DecreasesOpBuild(MlirOpBuilder builder, MlirLocation location, MlirValue value)
Build a llzk::verif::DecreasesOp Operation.
void llzkVerif_IncludeOpSetNumDimsPerMap(MlirOperation op, MlirAttribute attr)
Set NumDimsPerMap attribute of llzk::verif::IncludeOp Operation.
void llzkVerif_ContractOpSetTarget(MlirOperation op, MlirAttribute attr)
Set Target attribute of llzk::verif::ContractOp Operation.
void llzkVerif_EnsureConstrainOpSetCondition(MlirOperation op, MlirValue value)
Set Condition operand of llzk::verif::EnsureConstrainOp Operation.
MlirAttribute llzkVerif_IncludeOpGetCallee(MlirOperation op)
Get Callee attribute from llzk::verif::IncludeOp Operation.
bool llzkVerif_ContractOpIsDeclaration(MlirOperation inp)
Required by SymbolOpInterface.
MlirOperation llzkVerif_InvariantOpGetParentContract(MlirOperation inp)
Returns the contract operation that contains this invariant.
MlirOperation llzkVerif_StepYieldOpBuild(MlirOpBuilder builder, MlirLocation location, MlirValue value)
Build a llzk::verif::StepYieldOp Operation.
MlirValue llzkVerif_IncludeOpGetMapOperandsAt(MlirOperation op, intptr_t index)
Get MapOperands operand at index from llzk::verif::IncludeOp Operation.
void llzkVerif_ContractOpSetArgAttrs(MlirOperation op, MlirAttribute attr)
Set ArgAttrs attribute of llzk::verif::ContractOp Operation.
void llzkVerif_InvariantOpSetLoopName(MlirOperation op, MlirAttribute attr)
Set LoopName attribute of llzk::verif::InvariantOp Operation.
MlirOperation llzkVerif_EnsureComputeOpBuild(MlirOpBuilder builder, MlirLocation location, MlirValue condition)
Build a llzk::verif::EnsureComputeOp Operation.
MlirValue llzkVerif_RequireComputeOpGetCondition(MlirOperation op)
Get Condition operand from llzk::verif::RequireComputeOp Operation.
bool llzkOperationIsA_Verif_IncludeOp(MlirOperation inp)
Returns true if the Operation is a llzk::verif::IncludeOp.
void llzkVerif_InvariantOpSetLoopArgTypes(MlirOperation op, MlirAttribute attr)
Set LoopArgTypes attribute of llzk::verif::InvariantOp Operation.
MlirValue llzkVerif_IncludeOpGetArgOperandsAt(MlirOperation op, intptr_t index)
Get ArgOperands operand at index from llzk::verif::IncludeOp Operation.
void llzkVerif_RequireComputeOpSetCondition(MlirOperation op, MlirValue value)
Set Condition operand of llzk::verif::RequireComputeOp Operation.
void llzkVerif_IncludeOpSetMapOperands(MlirOperation op, intptr_t groupCount, MlirValueRange const *groups)
Set MapOperands operand groups of llzk::verif::IncludeOp Operation.
bool llzkOperationIsA_Verif_IncreasesOp(MlirOperation inp)
Returns true if the Operation is a llzk::verif::IncreasesOp.
bool llzkOperationIsA_Verif_StepOp(MlirOperation inp)
Returns true if the Operation is a llzk::verif::StepOp.
void llzkVerif_DecreasesOpSetValue(MlirOperation op, MlirValue value)
Set Value operand of llzk::verif::DecreasesOp Operation.
MlirRegion llzkVerif_InvariantOpGetRegion(MlirOperation op)
Get Region region from llzk::verif::InvariantOp Operation.
MlirValue llzkVerif_IncludeOpGetSelfValue(MlirOperation inp)
Return the "self" value (i.e.
MlirValue llzkVerif_IncreasesOpGetValue(MlirOperation op)
Get Value operand from llzk::verif::IncreasesOp Operation.
MlirType llzkVerif_IncludeOpGetTypeSignature(MlirOperation inp)
Return the FunctionType inferred from the arg operands of this CallOp.
void llzkVerif_OldOpSetValue(MlirOperation op, MlirValue value)
Set Value operand of llzk::verif::OldOp Operation.
MlirValue llzkVerif_EnsureComputeOpGetCondition(MlirOperation op)
Get Condition operand from llzk::verif::EnsureComputeOp Operation.
bool llzkOperationIsA_Verif_VerifAssertOp(MlirOperation inp)
Returns true if the Operation is a llzk::verif::VerifAssertOp.
MlirValue llzkVerif_EnsureConstrainOpGetCondition(MlirOperation op)
Get Condition operand from llzk::verif::EnsureConstrainOp Operation.
MlirRegion llzkVerif_ContractOpGetCallableRegion(MlirOperation inp)
Required by FunctionOpInterface.
bool llzkOperationIsA_Verif_VerifProveOp(MlirOperation inp)
Returns true if the Operation is a llzk::verif::VerifProveOp.
MlirValue llzkVerif_RequireConstrainOpGetCondition(MlirOperation op)
Get Condition operand from llzk::verif::RequireConstrainOp Operation.
bool llzkVerif_ContractOpHasFuncTarget(MlirOperation inp)
Return true iff the contract targets a function.
MlirOperation llzkVerif_VerifAssertOpBuild(MlirOpBuilder builder, MlirLocation location, MlirValue condition)
Build a llzk::verif::VerifAssertOp Operation.
bool llzkOperationIsA_Verif_ContractOp(MlirOperation inp)
Returns true if the Operation is a llzk::verif::ContractOp.
MlirAttribute llzkVerif_ContractOpGetFullyQualifiedName(MlirOperation inp, bool requireParent)
Return the full name for this contract from the root module, including all surrounding symbol table n...
MlirValue llzkVerif_OldOpGetResult(MlirOperation op)
Get Result result from llzk::verif::OldOp Operation.
void llzkVerif_ContractOpSetFunctionType(MlirOperation op, MlirAttribute attr)
Set FunctionType attribute of llzk::verif::ContractOp Operation.
MlirValue llzkVerif_DecreasesOpGetValue(MlirOperation op)
Get Value operand from llzk::verif::DecreasesOp Operation.
void llzkVerif_ContractOpSetSymName(MlirOperation op, MlirAttribute attr)
Set SymName attribute of llzk::verif::ContractOp Operation.
bool llzkOperationIsA_Verif_OldOp(MlirOperation inp)
Returns true if the Operation is a llzk::verif::OldOp.
MlirOperation llzkVerif_IncludeOpResolveCallable(MlirOperation inp)
Required by CallOpInterface.
Representation of an mlir::ValueRange
intptr_t size
Number of values in the range.