LLZK 3.0.0
An open-source IR for Zero Knowledge (ZK) circuits
Loading...
Searching...
No Matches
Ops.capi.cpp.inc
Go to the documentation of this file.
1/*===- TableGen'erated file -------------------------------------*- C++ -*-===*\
2|* *|
3|* Op C API Definitions *|
4|* *|
5|* Automatically generated file, do not edit! *|
6|* From: Ops.td *|
7|* *|
8\*===----------------------------------------------------------------------===*/
9
10
11#include <limits>
12
13using namespace mlir;
14using namespace llvm;
15
16MlirOperation llzkVerif_AssumeDetOpBuild(MlirOpBuilder builder, MlirLocation location, MlirValue hint) {
17 MlirOperationState state = mlirOperationStateGet(mlirStringRefCreateFromCString("verif.det.assume"), location);
18 mlirOperationStateAddOperands(&state, 1, &hint);
19
20 return mlirOpBuilderInsert(builder, mlirOperationCreate(&state));
21}
22
23bool llzkOperationIsA_Verif_AssumeDetOp(MlirOperation inp) {
24 return llvm::isa<AssumeDetOp>(unwrap(inp));
25}
26
27MlirValue llzkVerif_AssumeDetOpGetHint(MlirOperation op) {
28 auto range = llvm::cast<AssumeDetOp>(unwrap(op)).getODSOperandIndexAndLength(0);
29 assert(range.second == 1 && "expected fixed operand segment size");
30 assert(
31 static_cast<uintptr_t>(range.first) <= static_cast<uintptr_t>(std::numeric_limits<intptr_t>::max()) &&
32 "operand index exceeds intptr_t range"
33 );
34 return mlirOperationGetOperand(op, static_cast<intptr_t>(range.first));
35}
36
37void llzkVerif_AssumeDetOpSetHint(MlirOperation op, MlirValue value) {
38 auto range = llvm::cast<AssumeDetOp>(unwrap(op)).getODSOperandIndexAndLength(0);
39 assert(range.second == 1 && "expected fixed operand segment size");
40 assert(
41 static_cast<uintptr_t>(range.first) <= static_cast<uintptr_t>(std::numeric_limits<intptr_t>::max()) &&
42 "operand index exceeds intptr_t range"
43 );
44 mlirOperationSetOperand(op, static_cast<intptr_t>(range.first), value);
45}
46
47MlirOperation llzkVerif_ContractEndOpBuild(MlirOpBuilder builder, MlirLocation location) {
48 MlirOperationState state = mlirOperationStateGet(mlirStringRefCreateFromCString("verif.contract_end"), location);
49
50 return mlirOpBuilderInsert(builder, mlirOperationCreate(&state));
51}
52
53bool llzkOperationIsA_Verif_ContractEndOp(MlirOperation inp) {
54 return llvm::isa<ContractEndOp>(unwrap(inp));
55}
56
57bool llzkOperationIsA_Verif_ContractOp(MlirOperation inp) {
58 return llvm::isa<ContractOp>(unwrap(inp));
59}
60
61MlirAttribute llzkVerif_ContractOpGetSymName(MlirOperation op) {
62 return mlirOperationGetAttributeByName(op, mlirStringRefCreateFromCString("sym_name"));
63}
64
65void llzkVerif_ContractOpSetSymName(MlirOperation op, MlirAttribute attr) {
66 mlirOperationSetAttributeByName(op, mlirStringRefCreateFromCString("sym_name"), attr);
67}
68
69MlirAttribute llzkVerif_ContractOpGetTarget(MlirOperation op) {
70 return mlirOperationGetAttributeByName(op, mlirStringRefCreateFromCString("target"));
71}
72
73void llzkVerif_ContractOpSetTarget(MlirOperation op, MlirAttribute attr) {
74 mlirOperationSetAttributeByName(op, mlirStringRefCreateFromCString("target"), attr);
75}
76
77MlirAttribute llzkVerif_ContractOpGetFunctionType(MlirOperation op) {
78 return mlirOperationGetAttributeByName(op, mlirStringRefCreateFromCString("function_type"));
79}
80
81void llzkVerif_ContractOpSetFunctionType(MlirOperation op, MlirAttribute attr) {
82 mlirOperationSetAttributeByName(op, mlirStringRefCreateFromCString("function_type"), attr);
83}
84
85MlirAttribute llzkVerif_ContractOpGetArgAttrs(MlirOperation op) {
86 return mlirOperationGetAttributeByName(op, mlirStringRefCreateFromCString("arg_attrs"));
87}
88
89void llzkVerif_ContractOpSetArgAttrs(MlirOperation op, MlirAttribute attr) {
90 mlirOperationSetAttributeByName(op, mlirStringRefCreateFromCString("arg_attrs"), attr);
91}
92
93MlirRegion llzkVerif_ContractOpGetBody(MlirOperation op) {
94 return mlirOperationGetRegion(op, 0);
95}
96
97bool llzkVerif_ContractOpIsDeclaration(MlirOperation inp) {
98 return llvm::cast<ContractOp>(unwrap(inp)).isDeclaration();
99}
100
101bool llzkVerif_ContractOpHasArgPublicAttr(MlirOperation inp, unsigned index) {
102 return llvm::cast<ContractOp>(unwrap(inp)).hasArgPublicAttr(index);
103}
104
105bool llzkVerif_ContractOpHasFuncTarget(MlirOperation inp) {
106 return llvm::cast<ContractOp>(unwrap(inp)).hasFuncTarget();
107}
108
109bool llzkVerif_ContractOpHasStructTarget(MlirOperation inp) {
110 return llvm::cast<ContractOp>(unwrap(inp)).hasStructTarget();
111}
112
113MlirRegion llzkVerif_ContractOpGetCallableRegion(MlirOperation inp) {
114 return wrap(llvm::cast<ContractOp>(unwrap(inp)).getCallableRegion());
115}
116
117bool llzkVerif_ContractOpHasArgName(MlirOperation inp, unsigned index) {
118 return llvm::cast<ContractOp>(unwrap(inp)).hasArgName(index);
119}
120
121MlirAttribute llzkVerif_ContractOpGetFullyQualifiedName(MlirOperation inp, bool requireParent) {
122 return wrap(llvm::cast<ContractOp>(unwrap(inp)).getFullyQualifiedName(requireParent));
123}
124
125MlirOperation llzkVerif_DecreasesOpBuild(MlirOpBuilder builder, MlirLocation location, MlirValue value) {
126 MlirOperationState state = mlirOperationStateGet(mlirStringRefCreateFromCString("verif.decreases"), location);
127 mlirOperationStateAddOperands(&state, 1, &value);
128
129 return mlirOpBuilderInsert(builder, mlirOperationCreate(&state));
130}
131
132bool llzkOperationIsA_Verif_DecreasesOp(MlirOperation inp) {
133 return llvm::isa<DecreasesOp>(unwrap(inp));
134}
135
136MlirValue llzkVerif_DecreasesOpGetValue(MlirOperation op) {
137 auto range = llvm::cast<DecreasesOp>(unwrap(op)).getODSOperandIndexAndLength(0);
138 assert(range.second == 1 && "expected fixed operand segment size");
139 assert(
140 static_cast<uintptr_t>(range.first) <= static_cast<uintptr_t>(std::numeric_limits<intptr_t>::max()) &&
141 "operand index exceeds intptr_t range"
142 );
143 return mlirOperationGetOperand(op, static_cast<intptr_t>(range.first));
144}
145
146void llzkVerif_DecreasesOpSetValue(MlirOperation op, MlirValue value) {
147 auto range = llvm::cast<DecreasesOp>(unwrap(op)).getODSOperandIndexAndLength(0);
148 assert(range.second == 1 && "expected fixed operand segment size");
149 assert(
150 static_cast<uintptr_t>(range.first) <= static_cast<uintptr_t>(std::numeric_limits<intptr_t>::max()) &&
151 "operand index exceeds intptr_t range"
152 );
153 mlirOperationSetOperand(op, static_cast<intptr_t>(range.first), value);
154}
155
156MlirOperation llzkVerif_EnsureComputeOpBuild(MlirOpBuilder builder, MlirLocation location, MlirValue condition) {
157 MlirOperationState state = mlirOperationStateGet(mlirStringRefCreateFromCString("verif.ensure_compute"), location);
158 mlirOperationStateAddOperands(&state, 1, &condition);
159
160 return mlirOpBuilderInsert(builder, mlirOperationCreate(&state));
161}
162
164 return llvm::isa<EnsureComputeOp>(unwrap(inp));
165}
166
167MlirValue llzkVerif_EnsureComputeOpGetCondition(MlirOperation op) {
168 auto range = llvm::cast<EnsureComputeOp>(unwrap(op)).getODSOperandIndexAndLength(0);
169 assert(range.second == 1 && "expected fixed operand segment size");
170 assert(
171 static_cast<uintptr_t>(range.first) <= static_cast<uintptr_t>(std::numeric_limits<intptr_t>::max()) &&
172 "operand index exceeds intptr_t range"
173 );
174 return mlirOperationGetOperand(op, static_cast<intptr_t>(range.first));
175}
176
177void llzkVerif_EnsureComputeOpSetCondition(MlirOperation op, MlirValue value) {
178 auto range = llvm::cast<EnsureComputeOp>(unwrap(op)).getODSOperandIndexAndLength(0);
179 assert(range.second == 1 && "expected fixed operand segment size");
180 assert(
181 static_cast<uintptr_t>(range.first) <= static_cast<uintptr_t>(std::numeric_limits<intptr_t>::max()) &&
182 "operand index exceeds intptr_t range"
183 );
184 mlirOperationSetOperand(op, static_cast<intptr_t>(range.first), value);
185}
186
187MlirOperation llzkVerif_EnsureConstrainOpBuild(MlirOpBuilder builder, MlirLocation location, MlirValue condition) {
188 MlirOperationState state = mlirOperationStateGet(mlirStringRefCreateFromCString("verif.ensure_constrain"), location);
189 mlirOperationStateAddOperands(&state, 1, &condition);
190
191 return mlirOpBuilderInsert(builder, mlirOperationCreate(&state));
192}
193
195 return llvm::isa<EnsureConstrainOp>(unwrap(inp));
196}
197
198MlirValue llzkVerif_EnsureConstrainOpGetCondition(MlirOperation op) {
199 auto range = llvm::cast<EnsureConstrainOp>(unwrap(op)).getODSOperandIndexAndLength(0);
200 assert(range.second == 1 && "expected fixed operand segment size");
201 assert(
202 static_cast<uintptr_t>(range.first) <= static_cast<uintptr_t>(std::numeric_limits<intptr_t>::max()) &&
203 "operand index exceeds intptr_t range"
204 );
205 return mlirOperationGetOperand(op, static_cast<intptr_t>(range.first));
206}
207
208void llzkVerif_EnsureConstrainOpSetCondition(MlirOperation op, MlirValue value) {
209 auto range = llvm::cast<EnsureConstrainOp>(unwrap(op)).getODSOperandIndexAndLength(0);
210 assert(range.second == 1 && "expected fixed operand segment size");
211 assert(
212 static_cast<uintptr_t>(range.first) <= static_cast<uintptr_t>(std::numeric_limits<intptr_t>::max()) &&
213 "operand index exceeds intptr_t range"
214 );
215 mlirOperationSetOperand(op, static_cast<intptr_t>(range.first), value);
216}
217
218bool llzkOperationIsA_Verif_IncludeOp(MlirOperation inp) {
219 return llvm::isa<IncludeOp>(unwrap(inp));
220}
221
222intptr_t llzkVerif_IncludeOpGetArgOperandsCount(MlirOperation op) {
223 auto range = llvm::cast<IncludeOp>(unwrap(op)).getODSOperandIndexAndLength(0);
224 return range.second;
225}
226
227MlirValue llzkVerif_IncludeOpGetArgOperandsAt(MlirOperation op, intptr_t index) {
228 auto range = llvm::cast<IncludeOp>(unwrap(op)).getODSOperandIndexAndLength(0);
229 assert(index >= 0 && index < range.second && "variadic operand index out of range");
230 assert(
231 static_cast<uintptr_t>(range.first) <= static_cast<uintptr_t>(std::numeric_limits<intptr_t>::max()) &&
232 "operand index exceeds intptr_t range"
233 );
234 return mlirOperationGetOperand(op, static_cast<intptr_t>(range.first) + index);
235}
236
237void llzkVerif_IncludeOpSetArgOperands(MlirOperation op, intptr_t count, MlirValue const *values) {
238 if (count < 0)
239 return;
240 ::llvm::SmallVector<::mlir::Value> vals;
241 vals.reserve(static_cast<size_t>(count));
242 for (intptr_t i = 0; i < count; ++i)
243 vals.push_back(unwrap(values[i]));
244 ::llvm::cast<IncludeOp>(unwrap(op)).getArgOperandsMutable().assign(vals);
245}
246
247intptr_t llzkVerif_IncludeOpGetMapOperandsCount(MlirOperation op) {
248 auto range = llvm::cast<IncludeOp>(unwrap(op)).getODSOperandIndexAndLength(1);
249 return range.second;
250}
251
252MlirValue llzkVerif_IncludeOpGetMapOperandsAt(MlirOperation op, intptr_t index) {
253 auto range = llvm::cast<IncludeOp>(unwrap(op)).getODSOperandIndexAndLength(1);
254 assert(index >= 0 && index < range.second && "variadic operand index out of range");
255 assert(
256 static_cast<uintptr_t>(range.first) <= static_cast<uintptr_t>(std::numeric_limits<intptr_t>::max()) &&
257 "operand index exceeds intptr_t range"
258 );
259 return mlirOperationGetOperand(op, static_cast<intptr_t>(range.first) + index);
260}
261
262void llzkVerif_IncludeOpSetMapOperands(MlirOperation op, intptr_t groupCount, MlirValueRange const *groups) {
263 if (groupCount < 0)
264 return;
265
266 ::llvm::SmallVector<::mlir::Value> vals;
267 for (intptr_t g = 0; g < groupCount; ++g) {
268 assert(groups[g].size >= 0 && "group size must be non-negative");
269 for (intptr_t i = 0; i < groups[g].size; ++i) {
270 vals.push_back(unwrap(groups[g].values[i]));
271 }
272 }
273 ::llvm::cast<IncludeOp>(unwrap(op)).getMapOperandsMutable().join().assign(vals);
274
275 ::llvm::SmallVector<int32_t> newGroupSizes;
276 newGroupSizes.reserve(static_cast<size_t>(groupCount));
277 for (intptr_t g = 0; g < groupCount; ++g) {
278 assert(
279 groups[g].size <= static_cast<intptr_t>(std::numeric_limits<int32_t>::max()) &&
280 "group size exceeds int32_t range"
281 );
282 newGroupSizes.push_back(static_cast<int32_t>(groups[g].size));
283 }
284 MlirContext ctx = mlirOperationGetContext(op);
285 assert(
286 newGroupSizes.size() <= static_cast<size_t>(std::numeric_limits<intptr_t>::max()) &&
287 "group count exceeds intptr_t range"
288 );
289 mlirOperationSetAttributeByName(
290 op, mlirStringRefCreateFromCString("mapOpGroupSizes"),
291 mlirDenseI32ArrayGet(ctx, static_cast<intptr_t>(newGroupSizes.size()), newGroupSizes.data())
292 );
293}
294
295MlirAttribute llzkVerif_IncludeOpGetCallee(MlirOperation op) {
296 return mlirOperationGetAttributeByName(op, mlirStringRefCreateFromCString("callee"));
297}
298
299void llzkVerif_IncludeOpSetCallee(MlirOperation op, MlirAttribute attr) {
300 mlirOperationSetAttributeByName(op, mlirStringRefCreateFromCString("callee"), attr);
301}
302
303MlirAttribute llzkVerif_IncludeOpGetTemplateParams(MlirOperation op) {
304 return mlirOperationGetAttributeByName(op, mlirStringRefCreateFromCString("templateParams"));
305}
306
307void llzkVerif_IncludeOpSetTemplateParams(MlirOperation op, MlirAttribute attr) {
308 mlirOperationSetAttributeByName(op, mlirStringRefCreateFromCString("templateParams"), attr);
309}
310
311MlirAttribute llzkVerif_IncludeOpGetNumDimsPerMap(MlirOperation op) {
312 return mlirOperationGetAttributeByName(op, mlirStringRefCreateFromCString("numDimsPerMap"));
313}
314
315void llzkVerif_IncludeOpSetNumDimsPerMap(MlirOperation op, MlirAttribute attr) {
316 mlirOperationSetAttributeByName(op, mlirStringRefCreateFromCString("numDimsPerMap"), attr);
317}
318
319MlirAttribute llzkVerif_IncludeOpGetMapOpGroupSizes(MlirOperation op) {
320 return mlirOperationGetAttributeByName(op, mlirStringRefCreateFromCString("mapOpGroupSizes"));
321}
322
323void llzkVerif_IncludeOpSetMapOpGroupSizes(MlirOperation op, MlirAttribute attr) {
324 mlirOperationSetAttributeByName(op, mlirStringRefCreateFromCString("mapOpGroupSizes"), attr);
325}
326
328 return llvm::cast<IncludeOp>(unwrap(inp)).contractTargetsStruct();
329}
330
331MlirValue llzkVerif_IncludeOpGetSelfValue(MlirOperation inp) {
332 return wrap(llvm::cast<IncludeOp>(unwrap(inp)).getSelfValue());
333}
334
335MlirType llzkVerif_IncludeOpGetTypeSignature(MlirOperation inp) {
336 return wrap(llvm::cast<IncludeOp>(unwrap(inp)).getTypeSignature());
337}
338
339MlirOperation llzkVerif_IncludeOpResolveCallable(MlirOperation inp) {
340 return wrap(llvm::cast<IncludeOp>(unwrap(inp)).resolveCallable());
341}
342
343MlirOperation llzkVerif_IncreasesOpBuild(MlirOpBuilder builder, MlirLocation location, MlirValue value) {
344 MlirOperationState state = mlirOperationStateGet(mlirStringRefCreateFromCString("verif.increases"), location);
345 mlirOperationStateAddOperands(&state, 1, &value);
346
347 return mlirOpBuilderInsert(builder, mlirOperationCreate(&state));
348}
349
350bool llzkOperationIsA_Verif_IncreasesOp(MlirOperation inp) {
351 return llvm::isa<IncreasesOp>(unwrap(inp));
352}
353
354MlirValue llzkVerif_IncreasesOpGetValue(MlirOperation op) {
355 auto range = llvm::cast<IncreasesOp>(unwrap(op)).getODSOperandIndexAndLength(0);
356 assert(range.second == 1 && "expected fixed operand segment size");
357 assert(
358 static_cast<uintptr_t>(range.first) <= static_cast<uintptr_t>(std::numeric_limits<intptr_t>::max()) &&
359 "operand index exceeds intptr_t range"
360 );
361 return mlirOperationGetOperand(op, static_cast<intptr_t>(range.first));
362}
363
364void llzkVerif_IncreasesOpSetValue(MlirOperation op, MlirValue value) {
365 auto range = llvm::cast<IncreasesOp>(unwrap(op)).getODSOperandIndexAndLength(0);
366 assert(range.second == 1 && "expected fixed operand segment size");
367 assert(
368 static_cast<uintptr_t>(range.first) <= static_cast<uintptr_t>(std::numeric_limits<intptr_t>::max()) &&
369 "operand index exceeds intptr_t range"
370 );
371 mlirOperationSetOperand(op, static_cast<intptr_t>(range.first), value);
372}
373
374bool llzkOperationIsA_Verif_InvariantOp(MlirOperation inp) {
375 return llvm::isa<InvariantOp>(unwrap(inp));
376}
377
378MlirAttribute llzkVerif_InvariantOpGetLoopName(MlirOperation op) {
379 return mlirOperationGetAttributeByName(op, mlirStringRefCreateFromCString("loop_name"));
380}
381
382void llzkVerif_InvariantOpSetLoopName(MlirOperation op, MlirAttribute attr) {
383 mlirOperationSetAttributeByName(op, mlirStringRefCreateFromCString("loop_name"), attr);
384}
385
386MlirAttribute llzkVerif_InvariantOpGetLoopArgTypes(MlirOperation op) {
387 return mlirOperationGetAttributeByName(op, mlirStringRefCreateFromCString("loop_arg_types"));
388}
389
390void llzkVerif_InvariantOpSetLoopArgTypes(MlirOperation op, MlirAttribute attr) {
391 mlirOperationSetAttributeByName(op, mlirStringRefCreateFromCString("loop_arg_types"), attr);
392}
393
394MlirRegion llzkVerif_InvariantOpGetRegion(MlirOperation op) {
395 return mlirOperationGetRegion(op, 0);
396}
397
398MlirOperation llzkVerif_InvariantOpGetParentContract(MlirOperation inp) {
399 return wrap(llvm::cast<InvariantOp>(unwrap(inp)).getParentContract());
400}
401
402MlirOperation llzkVerif_OldOpBuild(MlirOpBuilder builder, MlirLocation location, MlirValue value) {
403 MlirOperationState state = mlirOperationStateGet(mlirStringRefCreateFromCString("verif.old"), location);
404 mlirOperationStateEnableResultTypeInference(&state);
405 mlirOperationStateAddOperands(&state, 1, &value);
406
407 return mlirOpBuilderInsert(builder, mlirOperationCreate(&state));
408}
409
410bool llzkOperationIsA_Verif_OldOp(MlirOperation inp) {
411 return llvm::isa<OldOp>(unwrap(inp));
412}
413
414MlirValue llzkVerif_OldOpGetValue(MlirOperation op) {
415 auto range = llvm::cast<OldOp>(unwrap(op)).getODSOperandIndexAndLength(0);
416 assert(range.second == 1 && "expected fixed operand segment size");
417 assert(
418 static_cast<uintptr_t>(range.first) <= static_cast<uintptr_t>(std::numeric_limits<intptr_t>::max()) &&
419 "operand index exceeds intptr_t range"
420 );
421 return mlirOperationGetOperand(op, static_cast<intptr_t>(range.first));
422}
423
424void llzkVerif_OldOpSetValue(MlirOperation op, MlirValue value) {
425 auto range = llvm::cast<OldOp>(unwrap(op)).getODSOperandIndexAndLength(0);
426 assert(range.second == 1 && "expected fixed operand segment size");
427 assert(
428 static_cast<uintptr_t>(range.first) <= static_cast<uintptr_t>(std::numeric_limits<intptr_t>::max()) &&
429 "operand index exceeds intptr_t range"
430 );
431 mlirOperationSetOperand(op, static_cast<intptr_t>(range.first), value);
432}
433
434MlirValue llzkVerif_OldOpGetResult(MlirOperation op) {
435 return mlirOperationGetResult(op, 0);
436}
437
438MlirOperation llzkVerif_ProveDetOpBuild(MlirOpBuilder builder, MlirLocation location, MlirValue condition) {
439 MlirOperationState state = mlirOperationStateGet(mlirStringRefCreateFromCString("verif.det.prove"), location);
440 mlirOperationStateEnableResultTypeInference(&state);
441 mlirOperationStateAddOperands(&state, 1, &condition);
442
443 return mlirOpBuilderInsert(builder, mlirOperationCreate(&state));
444}
445
446bool llzkOperationIsA_Verif_ProveDetOp(MlirOperation inp) {
447 return llvm::isa<ProveDetOp>(unwrap(inp));
448}
449
450MlirValue llzkVerif_ProveDetOpGetCondition(MlirOperation op) {
451 auto range = llvm::cast<ProveDetOp>(unwrap(op)).getODSOperandIndexAndLength(0);
452 assert(range.second == 1 && "expected fixed operand segment size");
453 assert(
454 static_cast<uintptr_t>(range.first) <= static_cast<uintptr_t>(std::numeric_limits<intptr_t>::max()) &&
455 "operand index exceeds intptr_t range"
456 );
457 return mlirOperationGetOperand(op, static_cast<intptr_t>(range.first));
458}
459
460void llzkVerif_ProveDetOpSetCondition(MlirOperation op, MlirValue value) {
461 auto range = llvm::cast<ProveDetOp>(unwrap(op)).getODSOperandIndexAndLength(0);
462 assert(range.second == 1 && "expected fixed operand segment size");
463 assert(
464 static_cast<uintptr_t>(range.first) <= static_cast<uintptr_t>(std::numeric_limits<intptr_t>::max()) &&
465 "operand index exceeds intptr_t range"
466 );
467 mlirOperationSetOperand(op, static_cast<intptr_t>(range.first), value);
468}
469
470MlirValue llzkVerif_ProveDetOpGetResult(MlirOperation op) {
471 return mlirOperationGetResult(op, 0);
472}
473
474MlirOperation llzkVerif_RequireComputeOpBuild(MlirOpBuilder builder, MlirLocation location, MlirValue condition) {
475 MlirOperationState state = mlirOperationStateGet(mlirStringRefCreateFromCString("verif.require_compute"), location);
476 mlirOperationStateAddOperands(&state, 1, &condition);
477
478 return mlirOpBuilderInsert(builder, mlirOperationCreate(&state));
479}
480
482 return llvm::isa<RequireComputeOp>(unwrap(inp));
483}
484
485MlirValue llzkVerif_RequireComputeOpGetCondition(MlirOperation op) {
486 auto range = llvm::cast<RequireComputeOp>(unwrap(op)).getODSOperandIndexAndLength(0);
487 assert(range.second == 1 && "expected fixed operand segment size");
488 assert(
489 static_cast<uintptr_t>(range.first) <= static_cast<uintptr_t>(std::numeric_limits<intptr_t>::max()) &&
490 "operand index exceeds intptr_t range"
491 );
492 return mlirOperationGetOperand(op, static_cast<intptr_t>(range.first));
493}
494
495void llzkVerif_RequireComputeOpSetCondition(MlirOperation op, MlirValue value) {
496 auto range = llvm::cast<RequireComputeOp>(unwrap(op)).getODSOperandIndexAndLength(0);
497 assert(range.second == 1 && "expected fixed operand segment size");
498 assert(
499 static_cast<uintptr_t>(range.first) <= static_cast<uintptr_t>(std::numeric_limits<intptr_t>::max()) &&
500 "operand index exceeds intptr_t range"
501 );
502 mlirOperationSetOperand(op, static_cast<intptr_t>(range.first), value);
503}
504
505MlirOperation llzkVerif_RequireConstrainOpBuild(MlirOpBuilder builder, MlirLocation location, MlirValue condition) {
506 MlirOperationState state = mlirOperationStateGet(mlirStringRefCreateFromCString("verif.require_constrain"), location);
507 mlirOperationStateAddOperands(&state, 1, &condition);
508
509 return mlirOpBuilderInsert(builder, mlirOperationCreate(&state));
510}
511
513 return llvm::isa<RequireConstrainOp>(unwrap(inp));
514}
515
516MlirValue llzkVerif_RequireConstrainOpGetCondition(MlirOperation op) {
517 auto range = llvm::cast<RequireConstrainOp>(unwrap(op)).getODSOperandIndexAndLength(0);
518 assert(range.second == 1 && "expected fixed operand segment size");
519 assert(
520 static_cast<uintptr_t>(range.first) <= static_cast<uintptr_t>(std::numeric_limits<intptr_t>::max()) &&
521 "operand index exceeds intptr_t range"
522 );
523 return mlirOperationGetOperand(op, static_cast<intptr_t>(range.first));
524}
525
526void llzkVerif_RequireConstrainOpSetCondition(MlirOperation op, MlirValue value) {
527 auto range = llvm::cast<RequireConstrainOp>(unwrap(op)).getODSOperandIndexAndLength(0);
528 assert(range.second == 1 && "expected fixed operand segment size");
529 assert(
530 static_cast<uintptr_t>(range.first) <= static_cast<uintptr_t>(std::numeric_limits<intptr_t>::max()) &&
531 "operand index exceeds intptr_t range"
532 );
533 mlirOperationSetOperand(op, static_cast<intptr_t>(range.first), value);
534}
535
536MlirOperation llzkVerif_StepOpBuild(MlirOpBuilder builder, MlirLocation location) {
537 MlirOperationState state = mlirOperationStateGet(mlirStringRefCreateFromCString("verif.step"), location);
538 llvm::SmallVector<MlirRegion, 1> regions;
539 regions.push_back(mlirRegionCreate());
540 mlirOperationStateAddOwnedRegions(&state, regions.size(), regions.data());
541
542 return mlirOpBuilderInsert(builder, mlirOperationCreate(&state));
543}
544
545bool llzkOperationIsA_Verif_StepOp(MlirOperation inp) {
546 return llvm::isa<StepOp>(unwrap(inp));
547}
548
549MlirRegion llzkVerif_StepOpGetRegion(MlirOperation op) {
550 return mlirOperationGetRegion(op, 0);
551}
552
553MlirOperation llzkVerif_StepYieldOpBuild(MlirOpBuilder builder, MlirLocation location, MlirValue value) {
554 MlirOperationState state = mlirOperationStateGet(mlirStringRefCreateFromCString("verif.step.yield"), location);
555 mlirOperationStateAddOperands(&state, 1, &value);
556
557 return mlirOpBuilderInsert(builder, mlirOperationCreate(&state));
558}
559
560bool llzkOperationIsA_Verif_StepYieldOp(MlirOperation inp) {
561 return llvm::isa<StepYieldOp>(unwrap(inp));
562}
563
564MlirValue llzkVerif_StepYieldOpGetValue(MlirOperation op) {
565 auto range = llvm::cast<StepYieldOp>(unwrap(op)).getODSOperandIndexAndLength(0);
566 assert(range.second == 1 && "expected fixed operand segment size");
567 assert(
568 static_cast<uintptr_t>(range.first) <= static_cast<uintptr_t>(std::numeric_limits<intptr_t>::max()) &&
569 "operand index exceeds intptr_t range"
570 );
571 return mlirOperationGetOperand(op, static_cast<intptr_t>(range.first));
572}
573
574void llzkVerif_StepYieldOpSetValue(MlirOperation op, MlirValue value) {
575 auto range = llvm::cast<StepYieldOp>(unwrap(op)).getODSOperandIndexAndLength(0);
576 assert(range.second == 1 && "expected fixed operand segment size");
577 assert(
578 static_cast<uintptr_t>(range.first) <= static_cast<uintptr_t>(std::numeric_limits<intptr_t>::max()) &&
579 "operand index exceeds intptr_t range"
580 );
581 mlirOperationSetOperand(op, static_cast<intptr_t>(range.first), value);
582}
583
584MlirOperation llzkVerif_VerifAssertOpBuild(MlirOpBuilder builder, MlirLocation location, MlirValue condition) {
585 MlirOperationState state = mlirOperationStateGet(mlirStringRefCreateFromCString("verif.assert"), location);
586 mlirOperationStateAddOperands(&state, 1, &condition);
587
588 return mlirOpBuilderInsert(builder, mlirOperationCreate(&state));
589}
590
592 return llvm::isa<VerifAssertOp>(unwrap(inp));
593}
594
595MlirValue llzkVerif_VerifAssertOpGetCondition(MlirOperation op) {
596 auto range = llvm::cast<VerifAssertOp>(unwrap(op)).getODSOperandIndexAndLength(0);
597 assert(range.second == 1 && "expected fixed operand segment size");
598 assert(
599 static_cast<uintptr_t>(range.first) <= static_cast<uintptr_t>(std::numeric_limits<intptr_t>::max()) &&
600 "operand index exceeds intptr_t range"
601 );
602 return mlirOperationGetOperand(op, static_cast<intptr_t>(range.first));
603}
604
605void llzkVerif_VerifAssertOpSetCondition(MlirOperation op, MlirValue value) {
606 auto range = llvm::cast<VerifAssertOp>(unwrap(op)).getODSOperandIndexAndLength(0);
607 assert(range.second == 1 && "expected fixed operand segment size");
608 assert(
609 static_cast<uintptr_t>(range.first) <= static_cast<uintptr_t>(std::numeric_limits<intptr_t>::max()) &&
610 "operand index exceeds intptr_t range"
611 );
612 mlirOperationSetOperand(op, static_cast<intptr_t>(range.first), value);
613}
614
615MlirOperation llzkVerif_VerifProveOpBuild(MlirOpBuilder builder, MlirLocation location, MlirValue condition) {
616 MlirOperationState state = mlirOperationStateGet(mlirStringRefCreateFromCString("verif.prove"), location);
617 mlirOperationStateAddOperands(&state, 1, &condition);
618
619 return mlirOpBuilderInsert(builder, mlirOperationCreate(&state));
620}
621
622bool llzkOperationIsA_Verif_VerifProveOp(MlirOperation inp) {
623 return llvm::isa<VerifProveOp>(unwrap(inp));
624}
625
626MlirValue llzkVerif_VerifProveOpGetCondition(MlirOperation op) {
627 auto range = llvm::cast<VerifProveOp>(unwrap(op)).getODSOperandIndexAndLength(0);
628 assert(range.second == 1 && "expected fixed operand segment size");
629 assert(
630 static_cast<uintptr_t>(range.first) <= static_cast<uintptr_t>(std::numeric_limits<intptr_t>::max()) &&
631 "operand index exceeds intptr_t range"
632 );
633 return mlirOperationGetOperand(op, static_cast<intptr_t>(range.first));
634}
635
636void llzkVerif_VerifProveOpSetCondition(MlirOperation op, MlirValue value) {
637 auto range = llvm::cast<VerifProveOp>(unwrap(op)).getODSOperandIndexAndLength(0);
638 assert(range.second == 1 && "expected fixed operand segment size");
639 assert(
640 static_cast<uintptr_t>(range.first) <= static_cast<uintptr_t>(std::numeric_limits<intptr_t>::max()) &&
641 "operand index exceeds intptr_t range"
642 );
643 mlirOperationSetOperand(op, static_cast<intptr_t>(range.first), value);
644}
645
646MlirOperation llzkVerif_VerifSMTProveOpBuild(MlirOpBuilder builder, MlirLocation location, MlirValue condition) {
647 MlirOperationState state = mlirOperationStateGet(mlirStringRefCreateFromCString("verif.smt_prove"), location);
648 mlirOperationStateAddOperands(&state, 1, &condition);
649
650 return mlirOpBuilderInsert(builder, mlirOperationCreate(&state));
651}
652
654 return llvm::isa<VerifSMTProveOp>(unwrap(inp));
655}
656
657MlirValue llzkVerif_VerifSMTProveOpGetCondition(MlirOperation op) {
658 auto range = llvm::cast<VerifSMTProveOp>(unwrap(op)).getODSOperandIndexAndLength(0);
659 assert(range.second == 1 && "expected fixed operand segment size");
660 assert(
661 static_cast<uintptr_t>(range.first) <= static_cast<uintptr_t>(std::numeric_limits<intptr_t>::max()) &&
662 "operand index exceeds intptr_t range"
663 );
664 return mlirOperationGetOperand(op, static_cast<intptr_t>(range.first));
665}
666
667void llzkVerif_VerifSMTProveOpSetCondition(MlirOperation op, MlirValue value) {
668 auto range = llvm::cast<VerifSMTProveOp>(unwrap(op)).getODSOperandIndexAndLength(0);
669 assert(range.second == 1 && "expected fixed operand segment size");
670 assert(
671 static_cast<uintptr_t>(range.first) <= static_cast<uintptr_t>(std::numeric_limits<intptr_t>::max()) &&
672 "operand index exceeds intptr_t range"
673 );
674 mlirOperationSetOperand(op, static_cast<intptr_t>(range.first), value);
675}
MlirOperation mlirOpBuilderInsert(MlirOpBuilder builder, MlirOperation op)
Inserts op at the current insertion point of builder and returns it.
Definition Builder.cpp:167
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_AssumeDetOpSetHint(MlirOperation op, MlirValue value)
Set Hint operand of llzk::verif::AssumeDetOp 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.
bool llzkOperationIsA_Verif_ProveDetOp(MlirOperation inp)
Returns true if the Operation is a llzk::verif::ProveDetOp.
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.
void llzkVerif_ProveDetOpSetCondition(MlirOperation op, MlirValue value)
Set Condition operand of llzk::verif::ProveDetOp 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.
MlirOperation llzkVerif_AssumeDetOpBuild(MlirOpBuilder builder, MlirLocation location, MlirValue hint)
Build a llzk::verif::AssumeDetOp 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.
MlirValue llzkVerif_ProveDetOpGetResult(MlirOperation op)
Get Result result from llzk::verif::ProveDetOp Operation.
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.
MlirValue llzkVerif_ProveDetOpGetCondition(MlirOperation op)
Get Condition operand from llzk::verif::ProveDetOp 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.
MlirOperation llzkVerif_ProveDetOpBuild(MlirOpBuilder builder, MlirLocation location, MlirValue condition)
Build a llzk::verif::ProveDetOp 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.
MlirValue llzkVerif_AssumeDetOpGetHint(MlirOperation op)
Get Hint operand from llzk::verif::AssumeDetOp 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...
bool llzkOperationIsA_Verif_AssumeDetOp(MlirOperation inp)
Returns true if the Operation is a llzk::verif::AssumeDetOp.
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.
Definition Support.h:47
intptr_t size
Number of values in the range.
Definition Support.h:51