diff --git a/changelogs/unreleased/th__non_native_felt_attr.yaml b/changelogs/unreleased/th__non_native_felt_attr.yaml new file mode 100644 index 000000000..1d76a5085 --- /dev/null +++ b/changelogs/unreleased/th__non_native_felt_attr.yaml @@ -0,0 +1,5 @@ +added: + - "Add `function.allow_non_native_field_ops` attribute" +changed: + - "Require `function.allow_non_native_field_ops` attribute on functions that use + non-native field operations, instead of requiring `function.allow_witness` attribute." diff --git a/include/llzk-c/Dialect/Function.h b/include/llzk-c/Dialect/Function.h index ed5989555..523673a4d 100644 --- a/include/llzk-c/Dialect/Function.h +++ b/include/llzk-c/Dialect/Function.h @@ -84,6 +84,12 @@ LLZK_DECLARE_OP_PREDICATE(FuncDefOp, HasAllowWitnessAttr); /// Sets the allow_witness attribute in the FuncDefOp operation. MLIR_CAPI_EXPORTED void llzkFuncDefOpSetAllowWitnessAttr(MlirOperation op, bool value); +/// Returns true if the FuncDefOp has the allow_non_native_field_ops attribute. +LLZK_DECLARE_OP_PREDICATE(FuncDefOp, HasAllowNonNativeFieldOpsAttr); + +/// Sets the allow_non_native_field_ops attribute in the FuncDefOp operation. +MLIR_CAPI_EXPORTED void llzkFuncDefOpSetAllowNonNativeFieldOpsAttr(MlirOperation op, bool value); + /// Returns true if the `idx`-th argument has the Pub attribute. LLZK_DECLARE_NARY_OP_PREDICATE(FuncDefOp, HasArgIsPub, unsigned arg); diff --git a/include/llzk/Dialect/Bool/IR/Ops.td b/include/llzk/Dialect/Bool/IR/Ops.td index c02355758..6cd18b958 100644 --- a/include/llzk/Dialect/Bool/IR/Ops.td +++ b/include/llzk/Dialect/Bool/IR/Ops.td @@ -39,7 +39,8 @@ class BoolUnaryOpBase traits = []> // Boolean operators //===------------------------------------------------------------------===// -def LLZK_AndBoolOp : BoolBinaryOpBase<"and", I1, [Commutative]> { +def LLZK_AndBoolOp + : BoolBinaryOpBase<"and", I1, [NotFieldNative, Commutative]> { let summary = "logical AND operator"; let description = [{ This operation computes the logical AND (i.e., conjunction) of two `i1` (i.e., boolean) @@ -49,7 +50,7 @@ def LLZK_AndBoolOp : BoolBinaryOpBase<"and", I1, [Commutative]> { }]; } -def LLZK_OrBoolOp : BoolBinaryOpBase<"or", I1, [Commutative]> { +def LLZK_OrBoolOp : BoolBinaryOpBase<"or", I1, [NotFieldNative, Commutative]> { let summary = "logical OR operator"; let description = [{ This operation computes the logical OR (i.e., disjunction) of two `i1` (i.e., boolean) @@ -59,7 +60,8 @@ def LLZK_OrBoolOp : BoolBinaryOpBase<"or", I1, [Commutative]> { }]; } -def LLZK_XorBoolOp : BoolBinaryOpBase<"xor", I1, [Commutative]> { +def LLZK_XorBoolOp + : BoolBinaryOpBase<"xor", I1, [NotFieldNative, Commutative]> { let summary = "logical XOR operator"; let description = [{ This operation computes the logical XOR (i.e., exclusive disjunction) of two `i1` (i.e., boolean) @@ -69,7 +71,7 @@ def LLZK_XorBoolOp : BoolBinaryOpBase<"xor", I1, [Commutative]> { }]; } -def LLZK_NotBoolOp : BoolUnaryOpBase<"not", I1, []> { +def LLZK_NotBoolOp : BoolUnaryOpBase<"not", I1, [NotFieldNative]> { let summary = "logical NOT operator"; let description = [{ This operation computes the logical NOT (i.e., negation) of an `i1` (i.e., boolean) diff --git a/include/llzk/Dialect/Felt/IR/Ops.td b/include/llzk/Dialect/Felt/IR/Ops.td index 1d328826a..3a0a41172 100644 --- a/include/llzk/Dialect/Felt/IR/Ops.td +++ b/include/llzk/Dialect/Felt/IR/Ops.td @@ -103,7 +103,8 @@ def LLZK_MulFeltOp : FeltDialectBinaryOp<"mul", LLZK_FeltType, [Commutative]> { let description = [{}]; } -def LLZK_PowFeltOp : FeltDialectBinaryOp<"pow", LLZK_FeltType, [WitnessGen]> { +def LLZK_PowFeltOp + : FeltDialectBinaryOp<"pow", LLZK_FeltType, [NotFieldNative]> { let summary = "exponentiation operator for field elements"; let description = [{ @@ -122,7 +123,7 @@ def LLZK_DivFeltOp : FeltDialectBinaryOp<"div", LLZK_FeltType> { } def LLZK_UnsignedIntDivFeltOp - : FeltDialectBinaryOp<"uintdiv", LLZK_FeltType, [WitnessGen]> { + : FeltDialectBinaryOp<"uintdiv", LLZK_FeltType, [NotFieldNative]> { let summary = "unsigned integer division operator for field elements"; let description = [{ Treats the operands as if they were unsigned integers with bitwidth @@ -131,7 +132,7 @@ def LLZK_UnsignedIntDivFeltOp } def LLZK_SignedIntDivFeltOp - : FeltDialectBinaryOp<"sintdiv", LLZK_FeltType, [WitnessGen]> { + : FeltDialectBinaryOp<"sintdiv", LLZK_FeltType, [NotFieldNative]> { let summary = "signed integer division operator for field elements"; let description = [{ Treats the operands as if they were signed integers with bitwidth @@ -148,7 +149,7 @@ def LLZK_SignedIntDivFeltOp } def LLZK_UnsignedModFeltOp - : FeltDialectBinaryOp<"umod", LLZK_FeltType, [WitnessGen]> { + : FeltDialectBinaryOp<"umod", LLZK_FeltType, [NotFieldNative]> { let summary = "unsigned integer modulus/remainder operator for field elements"; let description = [{ @@ -158,7 +159,7 @@ def LLZK_UnsignedModFeltOp } def LLZK_SignedModFeltOp - : FeltDialectBinaryOp<"smod", LLZK_FeltType, [WitnessGen]> { + : FeltDialectBinaryOp<"smod", LLZK_FeltType, [NotFieldNative]> { let summary = "signed integer modulus/remainder operator for field elements"; let description = [{ Computes the remainder that would result from the division operation performed @@ -171,31 +172,35 @@ def LLZK_NegFeltOp : FeltDialectUnaryOp<"neg", LLZK_FeltType> { let description = [{}]; } -def LLZK_InvFeltOp : FeltDialectUnaryOp<"inv", LLZK_FeltType, [WitnessGen]> { +def LLZK_InvFeltOp + : FeltDialectUnaryOp<"inv", LLZK_FeltType, [NotFieldNative]> { let summary = "inverse operator for field elements"; let description = [{}]; } def LLZK_AndFeltOp - : FeltDialectBinaryOp<"bit_and", LLZK_FeltType, [WitnessGen, Commutative]> { + : FeltDialectBinaryOp<"bit_and", + LLZK_FeltType, [NotFieldNative, Commutative]> { let summary = "bitwise AND operator for field elements"; let description = [{}]; } def LLZK_OrFeltOp - : FeltDialectBinaryOp<"bit_or", LLZK_FeltType, [WitnessGen, Commutative]> { + : FeltDialectBinaryOp<"bit_or", + LLZK_FeltType, [NotFieldNative, Commutative]> { let summary = "bitwise OR operator for field elements"; let description = [{}]; } def LLZK_XorFeltOp - : FeltDialectBinaryOp<"bit_xor", LLZK_FeltType, [WitnessGen, Commutative]> { + : FeltDialectBinaryOp<"bit_xor", + LLZK_FeltType, [NotFieldNative, Commutative]> { let summary = "bitwise XOR operator for field elements"; let description = [{}]; } def LLZK_NotFeltOp - : FeltDialectUnaryOp<"bit_not", LLZK_FeltType, [WitnessGen]> { + : FeltDialectUnaryOp<"bit_not", LLZK_FeltType, [NotFieldNative]> { let summary = "integer complement (bitwise-not) operator for field elements"; let description = [{ Treats the operand as an integer with a bitwidth equal to the bitwidth @@ -204,12 +209,14 @@ def LLZK_NotFeltOp }]; } -def LLZK_ShlFeltOp : FeltDialectBinaryOp<"shl", LLZK_FeltType, [WitnessGen]> { +def LLZK_ShlFeltOp + : FeltDialectBinaryOp<"shl", LLZK_FeltType, [NotFieldNative]> { let summary = "left shift operator for field elements"; let description = [{}]; } -def LLZK_ShrFeltOp : FeltDialectBinaryOp<"shr", LLZK_FeltType, [WitnessGen]> { +def LLZK_ShrFeltOp + : FeltDialectBinaryOp<"shr", LLZK_FeltType, [NotFieldNative]> { let summary = "right shift operator for field elements"; let description = [{}]; } diff --git a/include/llzk/Dialect/Function/IR/Attrs.td b/include/llzk/Dialect/Function/IR/Attrs.td index 788d63e79..12920a962 100644 --- a/include/llzk/Dialect/Function/IR/Attrs.td +++ b/include/llzk/Dialect/Function/IR/Attrs.td @@ -22,19 +22,31 @@ class FunctionDialectAttr { - let summary = "Marks functions to allow `ConstraintGen` ops"; + let summary = + "Marks functions to allow `ConstraintGen` ops within their body"; let description = [{ A unit attribute that can be attached to a `FuncDefOp` to indicate that ops - marked with `ConstraintGen` (ex: emit ops) are allowed within its body. + marked with `ConstraintGen` (e.g., emit ops) are allowed within its body. }]; } def LLZK_AllowWitnessAttr : FunctionDialectAttr<"AllowWitness", "allow_witness"> { - let summary = "Marks functions to allow `WitnessGen` ops"; + let summary = "Marks functions to allow `WitnessGen` ops within their body"; let description = [{ - A unit attribute that can be attached to a `FuncDefOp` to indicate that ops - marked with `WitnessGen` (i.e., boolean and bitwise ops) are allowed within its body. + A unit attribute that can be attached to a `FuncDefOp` to indicate that ops marked + with `WitnessGen` (e.g., construct and write ops) are allowed within its body. + }]; +} + +def LLZK_AllowNonNativeFieldOpsAttr + : FunctionDialectAttr<"AllowNonNativeFieldOps", + "allow_non_native_field_ops"> { + let summary = + "Marks functions to allow `NotFieldNative` ops within their body"; + let description = [{ + A unit attribute that can be attached to a `FuncDefOp` to indicate that ops marked + with `NotFieldNative` (e.g., boolean and bitwise ops) are allowed within its body. }]; } diff --git a/include/llzk/Dialect/Function/IR/OpTraits.h b/include/llzk/Dialect/Function/IR/OpTraits.h index 713dffdf0..b36b01175 100644 --- a/include/llzk/Dialect/Function/IR/OpTraits.h +++ b/include/llzk/Dialect/Function/IR/OpTraits.h @@ -17,6 +17,7 @@ namespace llzk::function { mlir::LogicalResult verifyConstraintGenTraitImpl(mlir::Operation *op); mlir::LogicalResult verifyWitnessGenTraitImpl(mlir::Operation *op); +mlir::LogicalResult verifyNotFieldNativeTraitImpl(mlir::Operation *op); /// Marker for ops that are specific to constraint generation. /// Verifies that the surrounding function is marked with the `AllowConstraintAttr`. @@ -38,4 +39,14 @@ class WitnessGen : public mlir::OpTrait::TraitBase { } }; +/// Marker for ops over `llzk.felt` type operands that are not native to finite field arithmetic. +/// Verifies that the surrounding function is marked with the `AllowNonNativeFieldOpsAttr`. +template +class NotFieldNative : public mlir::OpTrait::TraitBase { +public: + inline static mlir::LogicalResult verifyTrait(mlir::Operation *op) { + return verifyNotFieldNativeTraitImpl(op); + } +}; + } // namespace llzk::function diff --git a/include/llzk/Dialect/Function/IR/OpTraits.td b/include/llzk/Dialect/Function/IR/OpTraits.td index a7efd5bd5..86f42e5db 100644 --- a/include/llzk/Dialect/Function/IR/OpTraits.td +++ b/include/llzk/Dialect/Function/IR/OpTraits.td @@ -24,4 +24,12 @@ def ConstraintGen : NativeOpTrait<"ConstraintGen">, StructuralOpTrait { string cppNamespace = "::llzk::function"; } +/// Marker for ops over `llzk.felt` type operands that are not native to finite +/// field arithmetic and thus must be rewritten or folded into a constant after +/// the flattening and unrolling pass. Op classes with this trait are valid only +/// in functions that have the `AllowNonNativeFieldOpsAttr`. +def NotFieldNative : NativeOpTrait<"NotFieldNative">, StructuralOpTrait { + string cppNamespace = "::llzk::function"; +} + #endif // LLZK_FUNCTION_TRAITS diff --git a/include/llzk/Dialect/Function/IR/Ops.td b/include/llzk/Dialect/Function/IR/Ops.td index d7b9aba1e..d7d298de6 100644 --- a/include/llzk/Dialect/Function/IR/Ops.td +++ b/include/llzk/Dialect/Function/IR/Ops.td @@ -150,6 +150,14 @@ def FuncDefOp /// Add (resp. remove) the `allow_witness` attribute to (resp. from) the function def. void setAllowWitnessAttr(bool newValue = true); + /// Return `true` iff the function def has the `allow_non_native_field_ops` attribute. + inline bool hasAllowNonNativeFieldOpsAttr() { + return getOperation()->hasAttr(llzk::function::AllowNonNativeFieldOpsAttr::name); + } + + /// Add (resp. remove) the `allow_non_native_field_ops` attribute to (resp. from) the function def. + void setAllowNonNativeFieldOpsAttr(bool newValue = true); + /// Return `true` iff the argument at the given index has `pub` attribute. bool hasArgPublicAttr(unsigned index); diff --git a/lib/CAPI/Dialect/Function.cpp b/lib/CAPI/Dialect/Function.cpp index 759d3a175..0d5d13487 100644 --- a/lib/CAPI/Dialect/Function.cpp +++ b/lib/CAPI/Dialect/Function.cpp @@ -79,6 +79,14 @@ void llzkFuncDefOpSetAllowWitnessAttr(MlirOperation op, bool value) { unwrap_cast(op).setAllowWitnessAttr(value); } +bool llzkFuncDefOpGetHasAllowNonNativeFieldOpsAttr(MlirOperation op) { + return unwrap_cast(op).hasAllowNonNativeFieldOpsAttr(); +} + +void llzkFuncDefOpSetAllowNonNativeFieldOpsAttr(MlirOperation op, bool value) { + unwrap_cast(op).setAllowNonNativeFieldOpsAttr(value); +} + bool llzkFuncDefOpGetHasArgIsPub(MlirOperation op, unsigned argNo) { return unwrap_cast(op).hasArgPublicAttr(argNo); } diff --git a/lib/Dialect/Function/IR/OpTraits.cpp b/lib/Dialect/Function/IR/OpTraits.cpp index 4d6584763..b3cdd61d1 100644 --- a/lib/Dialect/Function/IR/OpTraits.cpp +++ b/lib/Dialect/Function/IR/OpTraits.cpp @@ -43,4 +43,12 @@ LogicalResult verifyWitnessGenTraitImpl(Operation *op) { return success(); } +LogicalResult verifyNotFieldNativeTraitImpl(Operation *op) { + if (!parentFuncDefOpHasAttr(op, &FuncDefOp::hasAllowNonNativeFieldOpsAttr)) { + return op->emitOpError() << "only valid within a '" << FuncDefOp::getOperationName() + << "' with '" << AllowNonNativeFieldOpsAttr::name << "' attribute"; + } + return success(); +} + } // namespace llzk::function diff --git a/lib/Dialect/Function/IR/Ops.cpp b/lib/Dialect/Function/IR/Ops.cpp index b178f49f3..8b4188188 100644 --- a/lib/Dialect/Function/IR/Ops.cpp +++ b/lib/Dialect/Function/IR/Ops.cpp @@ -213,6 +213,14 @@ void FuncDefOp::setAllowWitnessAttr(bool newValue) { } } +void FuncDefOp::setAllowNonNativeFieldOpsAttr(bool newValue) { + if (newValue) { + getOperation()->setAttr(AllowNonNativeFieldOpsAttr::name, UnitAttr::get(getContext())); + } else { + getOperation()->removeAttr(AllowNonNativeFieldOpsAttr::name); + } +} + bool FuncDefOp::hasArgPublicAttr(unsigned index) { if (index < this->getNumArguments()) { DictionaryAttr res = function_interface_impl::getArgAttrDict(*this, index); @@ -476,6 +484,9 @@ struct CallOpVerifier { if (target.hasAllowWitnessAttr() && !caller.hasAllowWitnessAttr()) { emitAttrErr(AllowWitnessAttr::name); } + if (target.hasAllowNonNativeFieldOpsAttr() && !caller.hasAllowNonNativeFieldOpsAttr()) { + emitAttrErr(AllowNonNativeFieldOpsAttr::name); + } } return aggregateRes; } diff --git a/test/Analysis/interval_analysis/edwards2montgomery.llzk b/test/Analysis/interval_analysis/edwards2montgomery.llzk index 9de2759fa..e958419fe 100644 --- a/test/Analysis/interval_analysis/edwards2montgomery.llzk +++ b/test/Analysis/interval_analysis/edwards2montgomery.llzk @@ -42,7 +42,7 @@ module attributes {veridise.lang = "llzk"} { } struct.def @EqzExt<[]> { struct.field @"$super" : !struct.type<@Component<[]>> - function.def @compute(%arg0: !array.type<4 x !felt.type>) -> !struct.type<@EqzExt<[]>> attributes {function.allow_witness} { + function.def @compute(%arg0: !array.type<4 x !felt.type>) -> !struct.type<@EqzExt<[]>> attributes {function.allow_non_native_field_ops, function.allow_witness} { %felt_const_0 = felt.const 0 %c3 = arith.constant 3 : index %c2 = arith.constant 2 : index @@ -93,7 +93,7 @@ module attributes {veridise.lang = "llzk"} { struct.field @"$super" : !struct.type<@NondetExtReg<[]>> struct.field @"$temp" : !struct.type<@EqzExt<[]>> struct.field @reg : !struct.type<@NondetExtReg<[]>> {column} - function.def @compute(%arg0: !array.type<4 x !felt.type>) -> !struct.type<@ExtReg<[]>> attributes {function.allow_witness} { + function.def @compute(%arg0: !array.type<4 x !felt.type>) -> !struct.type<@ExtReg<[]>> attributes {function.allow_non_native_field_ops, function.allow_witness} { %c3 = arith.constant 3 : index %c2 = arith.constant 2 : index %c1 = arith.constant 1 : index @@ -151,7 +151,7 @@ module attributes {veridise.lang = "llzk"} { struct.def @Div<[]> { struct.field @"$super" : !felt.type {llzk.pub} struct.field @reciprocal : !felt.type - function.def @compute(%arg0: !felt.type, %arg1: !felt.type) -> !struct.type<@Div<[]>> attributes {function.allow_witness} { + function.def @compute(%arg0: !felt.type, %arg1: !felt.type) -> !struct.type<@Div<[]>> attributes {function.allow_non_native_field_ops, function.allow_witness} { %self = struct.new : <@Div<[]>> %0 = felt.inv %arg1 : !felt.type struct.writef %self[@reciprocal] = %0 : <@Div<[]>>, !felt.type @@ -217,7 +217,7 @@ module attributes {veridise.lang = "llzk"} { struct.field @"$temp_0" : !struct.type<@Div<[]>> struct.field @"$temp" : !struct.type<@NondetReg<[]>> {column} struct.field @v : !struct.type<@Div<[]>> - function.def @compute(%arg0: !array.type<2 x !felt.type>) -> !struct.type<@Edwards2Montgomery<[]>> attributes {function.allow_witness} { + function.def @compute(%arg0: !array.type<2 x !felt.type>) -> !struct.type<@Edwards2Montgomery<[]>> attributes {function.allow_non_native_field_ops, function.allow_witness} { %felt_const_0 = felt.const 0 %felt_const_1 = felt.const 1 %self = struct.new : <@Edwards2Montgomery<[]>> diff --git a/test/Analysis/interval_analysis/interval_analysis_pass.llzk b/test/Analysis/interval_analysis/interval_analysis_pass.llzk index 87c91d1d3..e7594367b 100644 --- a/test/Analysis/interval_analysis/interval_analysis_pass.llzk +++ b/test/Analysis/interval_analysis/interval_analysis_pass.llzk @@ -134,7 +134,7 @@ module attributes {veridise.lang = "llzk"} { struct.def @Div<[]> { struct.field @"$super" : !felt.type struct.field @reciprocal : !felt.type - function.def @compute(%arg0: !felt.type, %arg1: !felt.type) -> !struct.type<@Div<[]>> { + function.def @compute(%arg0: !felt.type, %arg1: !felt.type) -> !struct.type<@Div<[]>> attributes {function.allow_non_native_field_ops} { %self = struct.new : <@Div<[]>> %0 = felt.inv %arg1 : !felt.type struct.writef %self[@reciprocal] = %0 : <@Div<[]>>, !felt.type diff --git a/test/Analysis/interval_analysis/interval_analysis_pass_compute.llzk b/test/Analysis/interval_analysis/interval_analysis_pass_compute.llzk index 8ed112901..70abee035 100644 --- a/test/Analysis/interval_analysis/interval_analysis_pass_compute.llzk +++ b/test/Analysis/interval_analysis/interval_analysis_pass_compute.llzk @@ -12,7 +12,7 @@ module attributes {veridise.lang = "llzk"} { struct.field @case7 : i1 struct.field @case8 : i1 - function.def @compute(%a: !felt.type) -> !struct.type<@BoolAnd> { + function.def @compute(%a: !felt.type) -> !struct.type<@BoolAnd> attributes {function.allow_non_native_field_ops} { %self = struct.new : !struct.type<@BoolAnd> %1 = felt.const 1 @@ -79,7 +79,7 @@ module attributes {veridise.lang = "llzk"} { struct.field @case7 : i1 struct.field @case8 : i1 - function.def @compute(%a: !felt.type) -> !struct.type<@BoolOr> { + function.def @compute(%a: !felt.type) -> !struct.type<@BoolOr> attributes {function.allow_non_native_field_ops} { %self = struct.new : !struct.type<@BoolOr> %1 = felt.const 1 @@ -146,7 +146,7 @@ module attributes {veridise.lang = "llzk"} { struct.field @case7 : i1 struct.field @case8 : i1 - function.def @compute(%a: !felt.type) -> !struct.type<@BoolXor> { + function.def @compute(%a: !felt.type) -> !struct.type<@BoolXor> attributes {function.allow_non_native_field_ops} { %self = struct.new : !struct.type<@BoolXor> %1 = felt.const 1 @@ -207,7 +207,7 @@ module attributes {veridise.lang = "llzk"} { struct.field @case1 : i1 struct.field @case2 : i1 - function.def @compute(%a: !felt.type) -> !struct.type<@BoolNot> { + function.def @compute(%a: !felt.type) -> !struct.type<@BoolNot> attributes {function.allow_non_native_field_ops} { %self = struct.new : !struct.type<@BoolNot> %1 = felt.const 1 @@ -251,7 +251,7 @@ module attributes {veridise.lang = "llzk"} { struct.field @case2 : !felt.type struct.field @case3 : !felt.type - function.def @compute(%a: !felt.type, %b: !felt.type) -> !struct.type<@BitAnd> { + function.def @compute(%a: !felt.type, %b: !felt.type) -> !struct.type<@BitAnd> attributes {function.allow_non_native_field_ops} { %self = struct.new : !struct.type<@BitAnd> %ff = felt.const 255 // 0xff @@ -296,7 +296,7 @@ module attributes {veridise.lang = "llzk"} { struct.field @case3 : !felt.type struct.field @case4 : !felt.type - function.def @compute(%a: !felt.type, %b: !felt.type) -> !struct.type<@ShiftLeft> { + function.def @compute(%a: !felt.type, %b: !felt.type) -> !struct.type<@ShiftLeft> attributes {function.allow_non_native_field_ops} { %self = struct.new : !struct.type<@ShiftLeft> %ff = felt.const 255 // 0xff @@ -344,7 +344,7 @@ module attributes {veridise.lang = "llzk"} { struct.field @case3 : !felt.type struct.field @case4 : !felt.type - function.def @compute(%a: !felt.type, %b: !felt.type) -> !struct.type<@ShiftRight> { + function.def @compute(%a: !felt.type, %b: !felt.type) -> !struct.type<@ShiftRight> attributes {function.allow_non_native_field_ops} { %self = struct.new : !struct.type<@ShiftRight> %ff = felt.const 255 // 0xff @@ -607,7 +607,7 @@ module attributes {veridise.lang = "llzk"} { module attributes {veridise.lang = "llzk"} { struct.def @ConstBools { struct.field @out : i1 - function.def @compute() -> !struct.type<@ConstBools> attributes {function.allow_witness} { + function.def @compute() -> !struct.type<@ConstBools> attributes {function.allow_non_native_field_ops, function.allow_witness} { %self = struct.new : !struct.type<@ConstBools> %true = arith.constant true %false = arith.constant false @@ -635,7 +635,7 @@ module attributes {veridise.lang = "llzk"} { function.return } - function.def @compute(%a: !felt.type, %b: !felt.type) -> !struct.type<@ArithConstraint> { + function.def @compute(%a: !felt.type, %b: !felt.type) -> !struct.type<@ArithConstraint> attributes {function.allow_non_native_field_ops} { %self = struct.new : !struct.type<@ArithConstraint> %5 = felt.const 5 diff --git a/test/Dialect/Bool/logic_ops_fail.llzk b/test/Dialect/Bool/logic_ops_fail.llzk index 90b50cfc8..5ea5e1356 100644 --- a/test/Dialect/Bool/logic_ops_fail.llzk +++ b/test/Dialect/Bool/logic_ops_fail.llzk @@ -3,14 +3,14 @@ function.def @f_and( %a: !felt.type, // expected-note {{prior use here}} %b: !felt.type -) -> i1 { +) -> i1 attributes {function.allow_non_native_field_ops} { // expected-error@+1 {{use of value '%a' expects different type than prior uses: 'i1' vs '!felt.type'}} %c = bool.and %a, %b function.return %c: i1 } // ----- -function.def @f_or(%a: !felt.type, %b: !felt.type) -> i1 attributes {function.allow_witness} { +function.def @f_or(%a: !felt.type, %b: !felt.type) -> i1 attributes {function.allow_non_native_field_ops} { // expected-error@+1 {{'bool.or' op operand #0 must be 1-bit signless integer or type variable, but got '!felt.type'}} %c = bool.or %a, %b : !felt.type, !felt.type function.return %c: i1 @@ -19,14 +19,14 @@ function.def @f_or(%a: !felt.type, %b: !felt.type) -> i1 attributes {function.al function.def @f_not1( %a: !array.type<4 x !felt.type> // expected-note {{prior use here}} -) -> i1 { +) -> i1 attributes {function.allow_non_native_field_ops} { // expected-error@+1 {{use of value '%a' expects different type than prior uses: 'i1' vs '!array.type<4 x !felt.type>'}} %c = bool.not %a function.return %c: i1 } // ----- -function.def @f_not2(%a: !array.type<4 x !felt.type>) -> i1 attributes {function.allow_witness} { +function.def @f_not2(%a: !array.type<4 x !felt.type>) -> i1 attributes {function.allow_non_native_field_ops} { // expected-error@+1 {{'bool.not' op operand #0 must be 1-bit signless integer or type variable, but got '!array.type<4 x !felt.type>'}} %c = bool.not %a : !array.type<4 x !felt.type> function.return %c: i1 diff --git a/test/Dialect/Bool/logic_ops_pass.llzk b/test/Dialect/Bool/logic_ops_pass.llzk index 08d35d51f..8318d9b80 100644 --- a/test/Dialect/Bool/logic_ops_pass.llzk +++ b/test/Dialect/Bool/logic_ops_pass.llzk @@ -1,44 +1,44 @@ // RUN: llzk-opt -split-input-file %s 2>&1 | FileCheck --enable-var-scope %s -function.def @f_and(%a: i1, %b: i1) -> i1 attributes {function.allow_witness} { +function.def @f_and(%a: i1, %b: i1) -> i1 attributes {function.allow_non_native_field_ops} { %c = bool.and %a, %b function.return %c: i1 } //CHECK-LABEL: function.def @f_and -//CHECK-SAME: (%[[A0:[0-9a-zA-Z_\.]+]]: i1, %[[A1:[0-9a-zA-Z_\.]+]]: i1) -> i1 attributes {function.allow_witness} { +//CHECK-SAME: (%[[A0:[0-9a-zA-Z_\.]+]]: i1, %[[A1:[0-9a-zA-Z_\.]+]]: i1) -> i1 attributes {function.allow_non_native_field_ops} { //CHECK-NEXT: %[[T1:[0-9a-zA-Z_\.]+]] = bool.and %[[A0]], %[[A1]] //CHECK-NEXT: function.return %[[T1]] : i1 //CHECK-NEXT: } // ----- -function.def @f_or(%a: i1, %b: i1) -> i1 attributes {function.allow_witness} { +function.def @f_or(%a: i1, %b: i1) -> i1 attributes {function.allow_non_native_field_ops} { %c = bool.or %a, %b function.return %c: i1 } //CHECK-LABEL: function.def @f_or -//CHECK-SAME: (%[[A0:[0-9a-zA-Z_\.]+]]: i1, %[[A1:[0-9a-zA-Z_\.]+]]: i1) -> i1 attributes {function.allow_witness} { +//CHECK-SAME: (%[[A0:[0-9a-zA-Z_\.]+]]: i1, %[[A1:[0-9a-zA-Z_\.]+]]: i1) -> i1 attributes {function.allow_non_native_field_ops} { //CHECK-NEXT: %[[T1:[0-9a-zA-Z_\.]+]] = bool.or %[[A0]], %[[A1]] //CHECK-NEXT: function.return %[[T1]] : i1 //CHECK-NEXT: } // ----- -function.def @f_xor(%a: i1, %b: i1) -> i1 attributes {function.allow_witness} { +function.def @f_xor(%a: i1, %b: i1) -> i1 attributes {function.allow_non_native_field_ops} { %c = bool.xor %a, %b function.return %c: i1 } //CHECK-LABEL: function.def @f_xor -//CHECK-SAME: (%[[A0:[0-9a-zA-Z_\.]+]]: i1, %[[A1:[0-9a-zA-Z_\.]+]]: i1) -> i1 attributes {function.allow_witness} { +//CHECK-SAME: (%[[A0:[0-9a-zA-Z_\.]+]]: i1, %[[A1:[0-9a-zA-Z_\.]+]]: i1) -> i1 attributes {function.allow_non_native_field_ops} { //CHECK-NEXT: %[[T1:[0-9a-zA-Z_\.]+]] = bool.xor %[[A0]], %[[A1]] //CHECK-NEXT: function.return %[[T1]] : i1 //CHECK-NEXT: } // ----- -function.def @f_not(%a: i1) -> i1 attributes {function.allow_witness} { +function.def @f_not(%a: i1) -> i1 attributes {function.allow_non_native_field_ops} { %c = bool.not %a function.return %c: i1 } //CHECK-LABEL: function.def @f_not -//CHECK-SAME: (%[[A0:[0-9a-zA-Z_\.]+]]: i1) -> i1 attributes {function.allow_witness} { +//CHECK-SAME: (%[[A0:[0-9a-zA-Z_\.]+]]: i1) -> i1 attributes {function.allow_non_native_field_ops} { //CHECK-NEXT: %[[T1:[0-9a-zA-Z_\.]+]] = bool.not %[[A0]] //CHECK-NEXT: function.return %[[T1]] : i1 //CHECK-NEXT: } diff --git a/test/Dialect/Felt/felt_arith_fail.llzk b/test/Dialect/Felt/felt_arith_fail.llzk index f4d73ab41..186b1b8c2 100644 --- a/test/Dialect/Felt/felt_arith_fail.llzk +++ b/test/Dialect/Felt/felt_arith_fail.llzk @@ -11,7 +11,7 @@ function.def @f_neg( function.def @f_inv( %a: index -) -> !felt.type attributes {function.allow_witness} { +) -> !felt.type attributes {function.allow_non_native_field_ops} { // expected-error@+1 {{'felt.inv' op operand #0 must be finite field element or type variable, but got 'index'}} %c = felt.inv %a : index function.return %c: !felt.type diff --git a/test/Dialect/Felt/felt_arith_pass.llzk b/test/Dialect/Felt/felt_arith_pass.llzk index 020ebf29a..4f38de5c2 100644 --- a/test/Dialect/Felt/felt_arith_pass.llzk +++ b/test/Dialect/Felt/felt_arith_pass.llzk @@ -45,12 +45,12 @@ function.def @f_mul(%a: !felt.type, %b: !felt.type) -> !felt.type { //CHECK-NEXT: } // ----- -function.def @f_pow(%a: !felt.type, %b: !felt.type) -> !felt.type attributes {function.allow_witness} { +function.def @f_pow(%a: !felt.type, %b: !felt.type) -> !felt.type attributes {function.allow_non_native_field_ops} { %c = felt.pow %a, %b function.return %c: !felt.type } //CHECK-LABEL: function.def @f_pow -//CHECK-SAME: (%[[A0:[0-9a-zA-Z_\.]+]]: !felt.type, %[[A1:[0-9a-zA-Z_\.]+]]: !felt.type) -> !felt.type attributes {function.allow_witness} { +//CHECK-SAME: (%[[A0:[0-9a-zA-Z_\.]+]]: !felt.type, %[[A1:[0-9a-zA-Z_\.]+]]: !felt.type) -> !felt.type attributes {function.allow_non_native_field_ops} { //CHECK-NEXT: %[[T1:[0-9a-zA-Z_\.]+]] = felt.pow %[[A0]], %[[A1]] //CHECK-NEXT: function.return %[[T1]] : !felt.type //CHECK-NEXT: } @@ -67,45 +67,45 @@ function.def @f_div(%a: !felt.type, %b: !felt.type) -> !felt.type { //CHECK-NEXT: } // ----- -function.def @f_uintdiv(%a: !felt.type, %b: !felt.type) -> !felt.type attributes {function.allow_witness} { +function.def @f_uintdiv(%a: !felt.type, %b: !felt.type) -> !felt.type attributes {function.allow_non_native_field_ops} { %c = felt.uintdiv %a, %b function.return %c: !felt.type } //CHECK-LABEL: function.def @f_uintdiv -//CHECK-SAME: (%[[A0:[0-9a-zA-Z_\.]+]]: !felt.type, %[[A1:[0-9a-zA-Z_\.]+]]: !felt.type) -> !felt.type attributes {function.allow_witness} { +//CHECK-SAME: (%[[A0:[0-9a-zA-Z_\.]+]]: !felt.type, %[[A1:[0-9a-zA-Z_\.]+]]: !felt.type) -> !felt.type attributes {function.allow_non_native_field_ops} { //CHECK-NEXT: %[[T1:[0-9a-zA-Z_\.]+]] = felt.uintdiv %[[A0]], %[[A1]] //CHECK-NEXT: function.return %[[T1]] : !felt.type //CHECK-NEXT: } // ----- -function.def @f_sintdiv(%a: !felt.type, %b: !felt.type) -> !felt.type attributes {function.allow_witness} { +function.def @f_sintdiv(%a: !felt.type, %b: !felt.type) -> !felt.type attributes {function.allow_non_native_field_ops} { %c = felt.sintdiv %a, %b function.return %c: !felt.type } //CHECK-LABEL: function.def @f_sintdiv -//CHECK-SAME: (%[[A0:[0-9a-zA-Z_\.]+]]: !felt.type, %[[A1:[0-9a-zA-Z_\.]+]]: !felt.type) -> !felt.type attributes {function.allow_witness} { +//CHECK-SAME: (%[[A0:[0-9a-zA-Z_\.]+]]: !felt.type, %[[A1:[0-9a-zA-Z_\.]+]]: !felt.type) -> !felt.type attributes {function.allow_non_native_field_ops} { //CHECK-NEXT: %[[T1:[0-9a-zA-Z_\.]+]] = felt.sintdiv %[[A0]], %[[A1]] //CHECK-NEXT: function.return %[[T1]] : !felt.type //CHECK-NEXT: } // ----- -function.def @f_umod(%a: !felt.type, %b: !felt.type) -> !felt.type attributes {function.allow_witness} { +function.def @f_umod(%a: !felt.type, %b: !felt.type) -> !felt.type attributes {function.allow_non_native_field_ops} { %c = felt.umod %a, %b function.return %c: !felt.type } //CHECK-LABEL: function.def @f_umod -//CHECK-SAME: (%[[A0:[0-9a-zA-Z_\.]+]]: !felt.type, %[[A1:[0-9a-zA-Z_\.]+]]: !felt.type) -> !felt.type attributes {function.allow_witness} { +//CHECK-SAME: (%[[A0:[0-9a-zA-Z_\.]+]]: !felt.type, %[[A1:[0-9a-zA-Z_\.]+]]: !felt.type) -> !felt.type attributes {function.allow_non_native_field_ops} { //CHECK-NEXT: %[[T1:[0-9a-zA-Z_\.]+]] = felt.umod %[[A0]], %[[A1]] //CHECK-NEXT: function.return %[[T1]] : !felt.type //CHECK-NEXT: } // ----- -function.def @f_smod(%a: !felt.type, %b: !felt.type) -> !felt.type attributes {function.allow_witness} { +function.def @f_smod(%a: !felt.type, %b: !felt.type) -> !felt.type attributes {function.allow_non_native_field_ops} { %c = felt.smod %a, %b function.return %c: !felt.type } //CHECK-LABEL: function.def @f_smod -//CHECK-SAME: (%[[A0:[0-9a-zA-Z_\.]+]]: !felt.type, %[[A1:[0-9a-zA-Z_\.]+]]: !felt.type) -> !felt.type attributes {function.allow_witness} { +//CHECK-SAME: (%[[A0:[0-9a-zA-Z_\.]+]]: !felt.type, %[[A1:[0-9a-zA-Z_\.]+]]: !felt.type) -> !felt.type attributes {function.allow_non_native_field_ops} { //CHECK-NEXT: %[[T1:[0-9a-zA-Z_\.]+]] = felt.smod %[[A0]], %[[A1]] //CHECK-NEXT: function.return %[[T1]] : !felt.type //CHECK-NEXT: } @@ -122,78 +122,78 @@ function.def @f_neg(%a: !felt.type) -> !felt.type { //CHECK-NEXT: } // ----- -function.def @f_inv(%a: !felt.type) -> !felt.type attributes {function.allow_witness} { +function.def @f_inv(%a: !felt.type) -> !felt.type attributes {function.allow_non_native_field_ops} { %c = felt.inv %a function.return %c: !felt.type } //CHECK-LABEL: function.def @f_inv -//CHECK-SAME: (%[[A0:[0-9a-zA-Z_\.]+]]: !felt.type) -> !felt.type attributes {function.allow_witness} { +//CHECK-SAME: (%[[A0:[0-9a-zA-Z_\.]+]]: !felt.type) -> !felt.type attributes {function.allow_non_native_field_ops} { //CHECK-NEXT: %[[T1:[0-9a-zA-Z_\.]+]] = felt.inv %[[A0]] //CHECK-NEXT: function.return %[[T1]] : !felt.type //CHECK-NEXT: } // ----- -function.def @f_bit_and(%a: !felt.type, %b: !felt.type) -> !felt.type attributes {function.allow_witness} { +function.def @f_bit_and(%a: !felt.type, %b: !felt.type) -> !felt.type attributes {function.allow_non_native_field_ops} { %c = felt.bit_and %a, %b function.return %c: !felt.type } //CHECK-LABEL: function.def @f_bit_and -//CHECK-SAME: (%[[A0:[0-9a-zA-Z_\.]+]]: !felt.type, %[[A1:[0-9a-zA-Z_\.]+]]: !felt.type) -> !felt.type attributes {function.allow_witness} { +//CHECK-SAME: (%[[A0:[0-9a-zA-Z_\.]+]]: !felt.type, %[[A1:[0-9a-zA-Z_\.]+]]: !felt.type) -> !felt.type attributes {function.allow_non_native_field_ops} { //CHECK-NEXT: %[[T1:[0-9a-zA-Z_\.]+]] = felt.bit_and %[[A0]], %[[A1]] //CHECK-NEXT: function.return %[[T1]] : !felt.type //CHECK-NEXT: } // ----- -function.def @f_bit_or(%a: !felt.type, %b: !felt.type) -> !felt.type attributes {function.allow_witness} { +function.def @f_bit_or(%a: !felt.type, %b: !felt.type) -> !felt.type attributes {function.allow_non_native_field_ops} { %c = felt.bit_or %a, %b function.return %c: !felt.type } //CHECK-LABEL: function.def @f_bit_or -//CHECK-SAME: (%[[A0:[0-9a-zA-Z_\.]+]]: !felt.type, %[[A1:[0-9a-zA-Z_\.]+]]: !felt.type) -> !felt.type attributes {function.allow_witness} { +//CHECK-SAME: (%[[A0:[0-9a-zA-Z_\.]+]]: !felt.type, %[[A1:[0-9a-zA-Z_\.]+]]: !felt.type) -> !felt.type attributes {function.allow_non_native_field_ops} { //CHECK-NEXT: %[[T1:[0-9a-zA-Z_\.]+]] = felt.bit_or %[[A0]], %[[A1]] //CHECK-NEXT: function.return %[[T1]] : !felt.type //CHECK-NEXT: } // ----- -function.def @f_bit_xor(%a: !felt.type, %b: !felt.type) -> !felt.type attributes {function.allow_witness} { +function.def @f_bit_xor(%a: !felt.type, %b: !felt.type) -> !felt.type attributes {function.allow_non_native_field_ops} { %c = felt.bit_xor %a, %b function.return %c: !felt.type } //CHECK-LABEL: function.def @f_bit_xor -//CHECK-SAME: (%[[A0:[0-9a-zA-Z_\.]+]]: !felt.type, %[[A1:[0-9a-zA-Z_\.]+]]: !felt.type) -> !felt.type attributes {function.allow_witness} { +//CHECK-SAME: (%[[A0:[0-9a-zA-Z_\.]+]]: !felt.type, %[[A1:[0-9a-zA-Z_\.]+]]: !felt.type) -> !felt.type attributes {function.allow_non_native_field_ops} { //CHECK-NEXT: %[[T1:[0-9a-zA-Z_\.]+]] = felt.bit_xor %[[A0]], %[[A1]] //CHECK-NEXT: function.return %[[T1]] : !felt.type //CHECK-NEXT: } // ----- -function.def @f_bit_not(%a: !felt.type) -> !felt.type attributes {function.allow_witness} { +function.def @f_bit_not(%a: !felt.type) -> !felt.type attributes {function.allow_non_native_field_ops} { %c = felt.bit_not %a function.return %c: !felt.type } //CHECK-LABEL: function.def @f_bit_not -//CHECK-SAME: (%[[A0:[0-9a-zA-Z_\.]+]]: !felt.type) -> !felt.type attributes {function.allow_witness} { +//CHECK-SAME: (%[[A0:[0-9a-zA-Z_\.]+]]: !felt.type) -> !felt.type attributes {function.allow_non_native_field_ops} { //CHECK-NEXT: %[[T1:[0-9a-zA-Z_\.]+]] = felt.bit_not %[[A0]] //CHECK-NEXT: function.return %[[T1]] : !felt.type //CHECK-NEXT: } // ----- -function.def @f_shl(%a: !felt.type, %b: !felt.type) -> !felt.type attributes {function.allow_witness} { +function.def @f_shl(%a: !felt.type, %b: !felt.type) -> !felt.type attributes {function.allow_non_native_field_ops} { %c = felt.shl %a, %b function.return %c: !felt.type } //CHECK-LABEL: function.def @f_shl -//CHECK-SAME: (%[[A0:[0-9a-zA-Z_\.]+]]: !felt.type, %[[A1:[0-9a-zA-Z_\.]+]]: !felt.type) -> !felt.type attributes {function.allow_witness} { +//CHECK-SAME: (%[[A0:[0-9a-zA-Z_\.]+]]: !felt.type, %[[A1:[0-9a-zA-Z_\.]+]]: !felt.type) -> !felt.type attributes {function.allow_non_native_field_ops} { //CHECK-NEXT: %[[T1:[0-9a-zA-Z_\.]+]] = felt.shl %[[A0]], %[[A1]] //CHECK-NEXT: function.return %[[T1]] : !felt.type //CHECK-NEXT: } // ----- -function.def @f_shr(%a: !felt.type, %b: !felt.type) -> !felt.type attributes {function.allow_witness} { +function.def @f_shr(%a: !felt.type, %b: !felt.type) -> !felt.type attributes {function.allow_non_native_field_ops} { %c = felt.shr %a, %b function.return %c: !felt.type } //CHECK-LABEL: function.def @f_shr -//CHECK-SAME: (%[[A0:[0-9a-zA-Z_\.]+]]: !felt.type, %[[A1:[0-9a-zA-Z_\.]+]]: !felt.type) -> !felt.type attributes {function.allow_witness} { +//CHECK-SAME: (%[[A0:[0-9a-zA-Z_\.]+]]: !felt.type, %[[A1:[0-9a-zA-Z_\.]+]]: !felt.type) -> !felt.type attributes {function.allow_non_native_field_ops} { //CHECK-NEXT: %[[T1:[0-9a-zA-Z_\.]+]] = felt.shr %[[A0]], %[[A1]] //CHECK-NEXT: function.return %[[T1]] : !felt.type //CHECK-NEXT: } diff --git a/test/Dialect/Function/function_restrictions_fail.llzk b/test/Dialect/Function/function_restrictions_fail.llzk index ed89ff893..a1c908f87 100644 --- a/test/Dialect/Function/function_restrictions_fail.llzk +++ b/test/Dialect/Function/function_restrictions_fail.llzk @@ -237,22 +237,7 @@ module attributes {veridise.lang = "llzk"} { } function.def @constrain(%self: !struct.type<@inv_in_constrain>, %a: !felt.type) { - // expected-error@+1 {{'felt.inv' op only valid within a 'function.def' with 'function.allow_witness' attribute}} - %c = felt.inv %a - function.return - } - } -} -// ----- -module attributes {veridise.lang = "llzk"} { - struct.def @inv_in_constrain { - function.def @compute(%a: !felt.type) -> !struct.type<@inv_in_constrain> { - %self = struct.new : !struct.type<@inv_in_constrain> - function.return %self : !struct.type<@inv_in_constrain> - } - - function.def @constrain(%self: !struct.type<@inv_in_constrain>, %a: !felt.type) { - // expected-error@+1 {{'felt.inv' op only valid within a 'function.def' with 'function.allow_witness' attribute}} + // expected-error@+1 {{'felt.inv' op only valid within a 'function.def' with 'function.allow_non_native_field_ops' attribute}} %c = felt.inv %a function.return } diff --git a/test/Dialect/Function/function_restrictions_pass.llzk b/test/Dialect/Function/function_restrictions_pass.llzk index 306cc6f47..ae3ad31e2 100644 --- a/test/Dialect/Function/function_restrictions_pass.llzk +++ b/test/Dialect/Function/function_restrictions_pass.llzk @@ -209,7 +209,7 @@ module attributes {veridise.lang = "llzk"} { module attributes {veridise.lang = "llzk"} { struct.def @inv_in_compute { - function.def @compute(%a: !felt.type) -> !struct.type<@inv_in_compute> { + function.def @compute(%a: !felt.type) -> !struct.type<@inv_in_compute> attributes {function.allow_non_native_field_ops} { %self = struct.new : !struct.type<@inv_in_compute> %c = felt.inv %a function.return %self : !struct.type<@inv_in_compute> @@ -222,7 +222,7 @@ module attributes {veridise.lang = "llzk"} { } //CHECK-LABEL: module attributes {veridise.lang = "llzk"} { //CHECK-NEXT: struct.def @inv_in_compute { -//CHECK-NEXT: function.def @compute(%arg0: !felt.type) -> !struct.type<@inv_in_compute> attributes {function.allow_witness} { +//CHECK-NEXT: function.def @compute(%arg0: !felt.type) -> !struct.type<@inv_in_compute> attributes {function.allow_non_native_field_ops, function.allow_witness} { //CHECK-NEXT: %self = struct.new : <@inv_in_compute> //CHECK-NEXT: %0 = felt.inv %arg0 //CHECK-NEXT: function.return %self : !struct.type<@inv_in_compute> @@ -233,6 +233,33 @@ module attributes {veridise.lang = "llzk"} { //CHECK-NEXT: } //CHECK-NEXT: } +// ----- +module attributes {veridise.lang = "llzk"} { + struct.def @inv_in_constrain { + function.def @compute(%a: !felt.type) -> !struct.type<@inv_in_constrain> { + %self = struct.new : !struct.type<@inv_in_constrain> + function.return %self : !struct.type<@inv_in_constrain> + } + + function.def @constrain(%self: !struct.type<@inv_in_constrain>, %a: !felt.type) attributes {function.allow_non_native_field_ops} { + %c = felt.inv %a + function.return + } + } +} +//CHECK-LABEL: module attributes {veridise.lang = "llzk"} { +//CHECK-NEXT: struct.def @inv_in_constrain { +//CHECK-NEXT: function.def @compute(%arg0: !felt.type) -> !struct.type<@inv_in_constrain> attributes {function.allow_witness} { +//CHECK-NEXT: %self = struct.new : <@inv_in_constrain> +//CHECK-NEXT: function.return %self : !struct.type<@inv_in_constrain> +//CHECK-NEXT: } +//CHECK-NEXT: function.def @constrain(%arg0: !struct.type<@inv_in_constrain>, %arg1: !felt.type) attributes {function.allow_constraint, function.allow_non_native_field_ops} { +//CHECK-NEXT: %0 = felt.inv %arg1 : !felt.type +//CHECK-NEXT: function.return +//CHECK-NEXT: } +//CHECK-NEXT: } +//CHECK-NEXT: } + // ----- // Ensure verifyStructTargetMatch() is not too restrictive; it will not prevent a global function call module attributes {veridise.lang = "llzk"} { diff --git a/test/Dialect/Include/include_pass.llzk b/test/Dialect/Include/include_pass.llzk index 7a79e9c3e..b55ae5957 100644 --- a/test/Dialect/Include/include_pass.llzk +++ b/test/Dialect/Include/include_pass.llzk @@ -178,7 +178,7 @@ module attributes {veridise.lang = "llzk"} { //CHECK-NEXT: struct.def @Div { //CHECK-NEXT: struct.field @reciprocal : !felt.type //CHECK-NEXT: struct.field @synthetic_return : !felt.type {llzk.pub} -//CHECK-NEXT: function.def @compute(%arg0: !felt.type, %arg1: !felt.type) -> !struct.type<@risc0::@Div> attributes {function.allow_witness} { +//CHECK-NEXT: function.def @compute(%arg0: !felt.type, %arg1: !felt.type) -> !struct.type<@risc0::@Div> attributes {function.allow_non_native_field_ops, function.allow_witness} { //CHECK-NEXT: %[[SELF:[0-9a-zA-Z_\.]+]] = struct.new : <@risc0::@Div> //CHECK-NEXT: %[[T0:[0-9a-zA-Z_\.]+]] = felt.inv %arg1 //CHECK-NEXT: struct.writef %[[SELF]][@reciprocal] = %[[T0]] : <@risc0::@Div>, !felt.type diff --git a/test/Dialect/Poly/typevar_pass.llzk b/test/Dialect/Poly/typevar_pass.llzk index 8b660e424..adf517555 100644 --- a/test/Dialect/Poly/typevar_pass.llzk +++ b/test/Dialect/Poly/typevar_pass.llzk @@ -497,7 +497,7 @@ module attributes {veridise.lang = "llzk"} { } struct.def @UnaryBool<[@T]> { - function.def @compute(%a: !poly.tvar<@T>) -> !struct.type<@UnaryBool<[@T]>> { + function.def @compute(%a: !poly.tvar<@T>) -> !struct.type<@UnaryBool<[@T]>> attributes {function.allow_non_native_field_ops} { %self = struct.new : !struct.type<@UnaryBool<[@T]>> %c = bool.not %a : !poly.tvar<@T> function.return %self : !struct.type<@UnaryBool<[@T]>> @@ -506,7 +506,7 @@ module attributes {veridise.lang = "llzk"} { } struct.def @BinaryBool<[@T, @U]> { - function.def @compute(%a: !poly.tvar<@T>, %b: !poly.tvar<@U>) -> !struct.type<@BinaryBool<[@T, @U]>> { + function.def @compute(%a: !poly.tvar<@T>, %b: !poly.tvar<@U>) -> !struct.type<@BinaryBool<[@T, @U]>> attributes {function.allow_non_native_field_ops} { %self = struct.new : !struct.type<@BinaryBool<[@T, @U]>> %c = bool.xor %a, %b : !poly.tvar<@T>, !poly.tvar<@U> function.return %self : !struct.type<@BinaryBool<[@T, @U]>> @@ -535,7 +535,7 @@ module attributes {veridise.lang = "llzk"} { //CHECK-NEXT: } //CHECK-NEXT: } //CHECK-LABEL: struct.def @UnaryBool<[@T]> { -//CHECK-NEXT: function.def @compute(%arg0: !poly.tvar<@T>) -> !struct.type<@UnaryBool<[@T]>> attributes {function.allow_witness} { +//CHECK-NEXT: function.def @compute(%arg0: !poly.tvar<@T>) -> !struct.type<@UnaryBool<[@T]>> attributes {function.allow_non_native_field_ops, function.allow_witness} { //CHECK-NEXT: %[[SELF:[0-9a-zA-Z_\.]+]] = struct.new : <@UnaryBool<[@T]>> //CHECK-NEXT: %[[T0:[0-9a-zA-Z_\.]+]] = bool.not %arg0 : !poly.tvar<@T> //CHECK-NEXT: function.return %[[SELF]] : !struct.type<@UnaryBool<[@T]>> @@ -545,7 +545,7 @@ module attributes {veridise.lang = "llzk"} { //CHECK-NEXT: } //CHECK-NEXT: } //CHECK-LABEL: struct.def @BinaryBool<[@T, @U]> { -//CHECK-NEXT: function.def @compute(%arg0: !poly.tvar<@T>, %arg1: !poly.tvar<@U>) -> !struct.type<@BinaryBool<[@T, @U]>> attributes {function.allow_witness} { +//CHECK-NEXT: function.def @compute(%arg0: !poly.tvar<@T>, %arg1: !poly.tvar<@U>) -> !struct.type<@BinaryBool<[@T, @U]>> attributes {function.allow_non_native_field_ops, function.allow_witness} { //CHECK-NEXT: %[[SELF:[0-9a-zA-Z_\.]+]] = struct.new : <@BinaryBool<[@T, @U]>> //CHECK-NEXT: %[[T0:[0-9a-zA-Z_\.]+]] = bool.xor %arg0, %arg1 : !poly.tvar<@T>, !poly.tvar<@U> //CHECK-NEXT: function.return %[[SELF]] : !struct.type<@BinaryBool<[@T, @U]>> diff --git a/test/FrontendLang/Circom/circomlib.llzk b/test/FrontendLang/Circom/circomlib.llzk index 5d24f338e..bb9051185 100644 --- a/test/FrontendLang/Circom/circomlib.llzk +++ b/test/FrontendLang/Circom/circomlib.llzk @@ -44,7 +44,7 @@ module attributes {veridise.lang = "llzk"} { struct.field @out: !felt.type {llzk.pub} struct.field @inv: !felt.type - function.def @compute(%in: !felt.type) -> !struct.type<@IsZero> { + function.def @compute(%in: !felt.type) -> !struct.type<@IsZero> attributes {function.allow_non_native_field_ops} { %self = struct.new : !struct.type<@IsZero> %const_1 = felt.const 1 %inv = felt.inv %in @@ -73,7 +73,7 @@ module attributes {veridise.lang = "llzk"} { // CHECK-LABEL: struct.def @IsZero { // CHECK-NEXT: struct.field @out : !felt.type {llzk.pub} // CHECK-NEXT: struct.field @inv : !felt.type - // CHECK-NEXT: function.def @compute(%[[V0:[0-9a-zA-Z_\.]+]]: !felt.type) -> !struct.type<@IsZero> attributes {function.allow_witness} { + // CHECK-NEXT: function.def @compute(%[[V0:[0-9a-zA-Z_\.]+]]: !felt.type) -> !struct.type<@IsZero> attributes {function.allow_non_native_field_ops, function.allow_witness} { // CHECK-NEXT: %[[V1:[0-9a-zA-Z_\.]+]] = struct.new : <@IsZero> // CHECK-NEXT: %[[V2:[0-9a-zA-Z_\.]+]] = felt.const 1 // CHECK-NEXT: %[[V3:[0-9a-zA-Z_\.]+]] = felt.inv %[[V0]] : !felt.type @@ -115,7 +115,7 @@ module attributes {veridise.lang = "llzk"} { struct.field @out: !felt.type {llzk.pub} struct.field @isz: !struct.type<@IsZero> - function.def @compute(%in: !array.type<2 x !felt.type>) -> !struct.type<@IsEqual> { + function.def @compute(%in: !array.type<2 x !felt.type>) -> !struct.type<@IsEqual> attributes {function.allow_non_native_field_ops} { %self = struct.new : !struct.type<@IsEqual> %0 = arith.constant 0 : index %1 = arith.constant 1 : index @@ -148,7 +148,7 @@ module attributes {veridise.lang = "llzk"} { // CHECK-LABEL: struct.def @IsEqual { // CHECK-NEXT: struct.field @out : !felt.type {llzk.pub} // CHECK-NEXT: struct.field @isz : !struct.type<@IsZero> - // CHECK-NEXT: function.def @compute(%[[V17:[0-9a-zA-Z_\.]+]]: !array.type<2 x !felt.type>) -> !struct.type<@IsEqual> attributes {function.allow_witness} { + // CHECK-NEXT: function.def @compute(%[[V17:[0-9a-zA-Z_\.]+]]: !array.type<2 x !felt.type>) -> !struct.type<@IsEqual> attributes {function.allow_non_native_field_ops, function.allow_witness} { // CHECK-NEXT: %[[V18:[0-9a-zA-Z_\.]+]] = struct.new : <@IsEqual> // CHECK-NEXT: %[[V19:[0-9a-zA-Z_\.]+]] = arith.constant 0 : index // CHECK-NEXT: %[[V20:[0-9a-zA-Z_\.]+]] = arith.constant 1 : index diff --git a/test/FrontendLang/Zirgen/Inputs/zir_example_loops.llzk b/test/FrontendLang/Zirgen/Inputs/zir_example_loops.llzk index 85133cb1e..57ef8e7c4 100644 --- a/test/FrontendLang/Zirgen/Inputs/zir_example_loops.llzk +++ b/test/FrontendLang/Zirgen/Inputs/zir_example_loops.llzk @@ -38,7 +38,7 @@ module attributes {veridise.lang = "llzk"} { } struct.def @EqzExt<[]> { struct.field @"$super" : !struct.type<@Component<[]>> - function.def @compute(%arg0: !array.type<4 x !felt.type>) -> !struct.type<@EqzExt<[]>> attributes {function.allow_witness} { + function.def @compute(%arg0: !array.type<4 x !felt.type>) -> !struct.type<@EqzExt<[]>> attributes {function.allow_non_native_field_ops, function.allow_witness} { %felt_const_0 = felt.const 0 %c3 = arith.constant 3 : index %c2 = arith.constant 2 : index @@ -89,7 +89,7 @@ module attributes {veridise.lang = "llzk"} { struct.field @"$super" : !struct.type<@NondetExtReg<[]>> struct.field @"$temp" : !struct.type<@EqzExt<[]>> struct.field @reg : !struct.type<@NondetExtReg<[]>> {column} - function.def @compute(%arg0: !array.type<4 x !felt.type>) -> !struct.type<@ExtReg<[]>> attributes {function.allow_witness} { + function.def @compute(%arg0: !array.type<4 x !felt.type>) -> !struct.type<@ExtReg<[]>> attributes {function.allow_non_native_field_ops, function.allow_witness} { %c3 = arith.constant 3 : index %c2 = arith.constant 2 : index %c1 = arith.constant 1 : index @@ -147,7 +147,7 @@ module attributes {veridise.lang = "llzk"} { struct.def @Div<[]> { struct.field @"$super" : !felt.type {llzk.pub} struct.field @reciprocal : !felt.type - function.def @compute(%arg0: !felt.type, %arg1: !felt.type) -> !struct.type<@Div<[]>> attributes {function.allow_witness} { + function.def @compute(%arg0: !felt.type, %arg1: !felt.type) -> !struct.type<@Div<[]>> attributes {function.allow_non_native_field_ops, function.allow_witness} { %self = struct.new : <@Div<[]>> %0 = felt.inv %arg1 : !felt.type struct.writef %self[@reciprocal] = %0 : <@Div<[]>>, !felt.type diff --git a/test/FrontendLang/Zirgen/mastermind.llzk b/test/FrontendLang/Zirgen/mastermind.llzk index ee36a8fb0..1adccef28 100644 --- a/test/FrontendLang/Zirgen/mastermind.llzk +++ b/test/FrontendLang/Zirgen/mastermind.llzk @@ -41,7 +41,7 @@ module attributes {veridise.lang = "llzk"} { } struct.def @EqzExt<[]> { struct.field @"$super" : !struct.type<@Component<[]>> - function.def @compute(%arg0: !array.type<4 x !felt.type>) -> !struct.type<@EqzExt<[]>> attributes {function.allow_witness} { + function.def @compute(%arg0: !array.type<4 x !felt.type>) -> !struct.type<@EqzExt<[]>> attributes {function.allow_non_native_field_ops, function.allow_witness} { %felt_const_0 = felt.const 0 %c3 = arith.constant 3 : index %c2 = arith.constant 2 : index @@ -92,7 +92,7 @@ module attributes {veridise.lang = "llzk"} { struct.field @"$super" : !struct.type<@NondetExtReg<[]>> struct.field @"$temp" : !struct.type<@EqzExt<[]>> struct.field @reg : !struct.type<@NondetExtReg<[]>> {column} - function.def @compute(%arg0: !array.type<4 x !felt.type>) -> !struct.type<@ExtReg<[]>> attributes {function.allow_witness} { + function.def @compute(%arg0: !array.type<4 x !felt.type>) -> !struct.type<@ExtReg<[]>> attributes {function.allow_non_native_field_ops, function.allow_witness} { %c3 = arith.constant 3 : index %c2 = arith.constant 2 : index %c1 = arith.constant 1 : index @@ -150,7 +150,7 @@ module attributes {veridise.lang = "llzk"} { struct.def @Div<[]> { struct.field @"$super" : !felt.type struct.field @reciprocal : !felt.type - function.def @compute(%arg0: !felt.type, %arg1: !felt.type) -> !struct.type<@Div<[]>> attributes {function.allow_witness} { + function.def @compute(%arg0: !felt.type, %arg1: !felt.type) -> !struct.type<@Div<[]>> attributes {function.allow_non_native_field_ops, function.allow_witness} { %self = struct.new : !struct.type<@Div<[]>> %0 = felt.inv %arg1 : !felt.type struct.writef %self[@reciprocal] = %0 : <@Div<[]>>, !felt.type @@ -2002,7 +2002,7 @@ module attributes {veridise.lang = "llzk"} { struct.field @inv : !struct.type<@NondetReg<[]>> {column} struct.field @"$temp" : !felt.type struct.field @isZero : !struct.type<@NondetReg<[]>> {column} - function.def @compute(%arg0: !felt.type) -> !struct.type<@IsZero<[]>> attributes {function.allow_witness} { + function.def @compute(%arg0: !felt.type) -> !struct.type<@IsZero<[]>> attributes {function.allow_non_native_field_ops, function.allow_witness} { %felt_const_0 = felt.const 0 %self = struct.new : !struct.type<@IsZero<[]>> %0 = bool.cmp eq(%arg0, %felt_const_0) @@ -2059,7 +2059,7 @@ module attributes {veridise.lang = "llzk"} { struct.def @Eq<[]> { struct.field @"$super" : !struct.type<@IsZero<[]>> {llzk.pub} struct.field @"$temp" : !struct.type<@IsZero<[]>> {column} - function.def @compute(%arg0: !felt.type, %arg1: !felt.type) -> !struct.type<@Eq<[]>> attributes {function.allow_witness} { + function.def @compute(%arg0: !felt.type, %arg1: !felt.type) -> !struct.type<@Eq<[]>> attributes {function.allow_non_native_field_ops, function.allow_witness} { %self = struct.new : !struct.type<@Eq<[]>> %0 = felt.sub %arg0, %arg1 : !felt.type, !felt.type %1 = function.call @IsZero::@compute(%0) : (!felt.type) -> !struct.type<@IsZero<[]>> @@ -2079,7 +2079,7 @@ module attributes {veridise.lang = "llzk"} { struct.field @"$super" : !struct.type<@Eq<[]>> struct.field @"$temp" : !struct.type<@Assert<[]>> struct.field @r : !struct.type<@Eq<[]>> {column} - function.def @compute(%arg0: !poly.tvar<@T>, %arg1: !poly.tvar<@T>) -> !struct.type<@EnsureEq<[@T]>> attributes {function.allow_witness} { + function.def @compute(%arg0: !poly.tvar<@T>, %arg1: !poly.tvar<@T>) -> !struct.type<@EnsureEq<[@T]>> attributes {function.allow_non_native_field_ops, function.allow_witness} { %0 = string.new "Provided values are not equal" %felt_const_0 = felt.const 0 %self = struct.new : !struct.type<@EnsureEq<[@T]>> @@ -2723,7 +2723,7 @@ module attributes {veridise.lang = "llzk"} { struct.field @"$temp_0" : !array.type<@N x !felt.type> struct.field @"$temp" : !array.type<@N x !struct.type<@IsZero<[]>>> {column} struct.field @"$array" : !array.type<@N x !struct.type<@IsZero<[]>>> {column} - function.def @compute(%arg0: !struct.type<@Pegs<[@N]>>, %arg1: !felt.type) -> !struct.type<@CountColors<[@N]>> attributes {function.allow_witness} { + function.def @compute(%arg0: !struct.type<@Pegs<[@N]>>, %arg1: !felt.type) -> !struct.type<@CountColors<[@N]>> attributes {function.allow_non_native_field_ops, function.allow_witness} { %felt_const_0 = felt.const 0 %c0 = arith.constant 0 : index %c1 = arith.constant 1 : index @@ -2909,7 +2909,7 @@ module attributes {veridise.lang = "llzk"} { struct.field @"$temp_0" : !array.type<#map x !struct.type<@EnsureEq<[!poly.tvar<@T>]>>> {column} struct.field @"$array" : !array.type<#map x !struct.type<@Component<[]>>> struct.field @"$temp" : !struct.type<@Zip<[!poly.tvar<@T>, !poly.tvar<@T>, @N]>> - function.def @compute(%arg0: !array.type<@N x !poly.tvar<@T>>, %arg1: !array.type<@N x !poly.tvar<@T>>) -> !struct.type<@AssertArrsEq<[@T, @N]>> attributes {function.allow_witness} { + function.def @compute(%arg0: !array.type<@N x !poly.tvar<@T>>, %arg1: !array.type<@N x !poly.tvar<@T>>) -> !struct.type<@AssertArrsEq<[@T, @N]>> attributes {function.allow_non_native_field_ops, function.allow_witness} { %c0 = arith.constant 0 : index %c1 = arith.constant 1 : index %self = struct.new : !struct.type<@AssertArrsEq<[@T, @N]>> @@ -2993,7 +2993,7 @@ module attributes {veridise.lang = "llzk"} { struct.field @"$temp_0" : !struct.type<@AssertArrsEq<[!felt.type, 24]>> struct.field @code : !struct.type<@SetCode<[@COLORS, @PEGS]>> struct.field @"$temp" : !struct.type<@CheckBounds<[@COLORS, @PEGS]>> - function.def @compute(%arg0: !struct.type<@Nonce<[]>>, %arg1: !struct.type<@Pegs<[@PEGS]>>, %arg2: !struct.type<@CodeHash<[]>>, %arg3: !struct.type<@Pegs<[@PEGS]>>) -> !struct.type<@MakeGuess<[@COLORS, @PEGS]>> attributes {function.allow_witness} { + function.def @compute(%arg0: !struct.type<@Nonce<[]>>, %arg1: !struct.type<@Pegs<[@PEGS]>>, %arg2: !struct.type<@CodeHash<[]>>, %arg3: !struct.type<@Pegs<[@PEGS]>>) -> !struct.type<@MakeGuess<[@COLORS, @PEGS]>> attributes {function.allow_non_native_field_ops, function.allow_witness} { %0 = string.new "Partial guesses: %u" %1 = string.new "Correct guesses: %u" %felt_const_0 = felt.const 0 @@ -3272,7 +3272,7 @@ module attributes {veridise.lang = "llzk"} { struct.field @"$super" : !struct.type<@MakeGuess<[@COLORS, @PEGS]>> struct.field @"$temp" : !struct.type<@Assert<[]>> struct.field @guess : !struct.type<@MakeGuess<[@COLORS, @PEGS]>> {column} - function.def @compute(%arg0: !struct.type<@Nonce<[]>>, %arg1: !struct.type<@Pegs<[@PEGS]>>, %arg2: !struct.type<@CodeHash<[]>>, %arg3: !struct.type<@Pegs<[@PEGS]>>) -> !struct.type<@MakeGuessWithChecks<[@COLORS, @PEGS]>> attributes {function.allow_witness} { + function.def @compute(%arg0: !struct.type<@Nonce<[]>>, %arg1: !struct.type<@Pegs<[@PEGS]>>, %arg2: !struct.type<@CodeHash<[]>>, %arg3: !struct.type<@Pegs<[@PEGS]>>) -> !struct.type<@MakeGuessWithChecks<[@COLORS, @PEGS]>> attributes {function.allow_non_native_field_ops, function.allow_witness} { %0 = string.new "Guess check post condition failed" %felt_const_1 = felt.const 1 %felt_const_0 = felt.const 0 diff --git a/test/FrontendLang/Zirgen/zir_example_0.llzk b/test/FrontendLang/Zirgen/zir_example_0.llzk index 4b43d9c94..40d366e40 100644 --- a/test/FrontendLang/Zirgen/zir_example_0.llzk +++ b/test/FrontendLang/Zirgen/zir_example_0.llzk @@ -41,7 +41,7 @@ module attributes {veridise.lang = "llzk"} { // ZIR frontend should mark function.return value with `pub` struct.field @synthetic_return : !felt.type {llzk.pub} - function.def @compute(%lhs: !felt.type, %rhs: !felt.type) -> !struct.type<@risc0::@Div> { + function.def @compute(%lhs: !felt.type, %rhs: !felt.type) -> !struct.type<@risc0::@Div> attributes {function.allow_non_native_field_ops} { %self = struct.new : !struct.type<@risc0::@Div> // res_inv := inv(rhs); %res_inv = felt.inv %rhs @@ -102,7 +102,7 @@ module attributes {veridise.lang = "llzk"} { //CHECK-NEXT: struct.def @Div { //CHECK-NEXT: struct.field @reciprocal : !felt.type //CHECK-NEXT: struct.field @synthetic_return : !felt.type {llzk.pub} -//CHECK-NEXT: function.def @compute(%[[A0:[0-9a-zA-Z_\.]+]]: !felt.type, %[[A1:[0-9a-zA-Z_\.]+]]: !felt.type) -> !struct.type<@risc0::@Div> attributes {function.allow_witness} { +//CHECK-NEXT: function.def @compute(%[[A0:[0-9a-zA-Z_\.]+]]: !felt.type, %[[A1:[0-9a-zA-Z_\.]+]]: !felt.type) -> !struct.type<@risc0::@Div> attributes {function.allow_non_native_field_ops, function.allow_witness} { //CHECK-NEXT: %[[SELF:[0-9a-zA-Z_\.]+]] = struct.new : <@risc0::@Div> //CHECK-NEXT: %[[T0:[0-9a-zA-Z_\.]+]] = felt.inv %[[A1]] //CHECK-NEXT: struct.writef %[[SELF]][@reciprocal] = %[[T0]] : <@risc0::@Div>, !felt.type diff --git a/test/FrontendLang/Zirgen/zir_example_2.llzk b/test/FrontendLang/Zirgen/zir_example_2.llzk index 84946d449..d52b45b52 100644 --- a/test/FrontendLang/Zirgen/zir_example_2.llzk +++ b/test/FrontendLang/Zirgen/zir_example_2.llzk @@ -138,7 +138,7 @@ module attributes {veridise.lang = "llzk"} { // ZIR frontend should mark function.return value with `pub` struct.field @synthetic_return: !felt.type {llzk.pub} - function.def @compute(%x: !struct.type<@std::@risc0::@ValU32>, %mode: !felt.type) -> !struct.type<@AddrDecomposeBits> { + function.def @compute(%x: !struct.type<@std::@risc0::@ValU32>, %mode: !felt.type) -> !struct.type<@AddrDecomposeBits> attributes {function.allow_non_native_field_ops} { %self = struct.new : !struct.type<@AddrDecomposeBits> // low0 := NondetBitReg.compute(x.low & 0x1); %t01 = struct.readf %x[@low] : !struct.type<@std::@risc0::@ValU32>, !felt.type @@ -360,7 +360,7 @@ module attributes {veridise.lang = "llzk"} { //CHECK-NEXT: struct.field @addr : !felt.type //CHECK-NEXT: struct.field @synthetic_return : !felt.type {llzk.pub} //CHECK-NEXT: function.def @compute(%[[A0:[0-9a-zA-Z_\.]+]]: !struct.type<@std::@risc0::@ValU32>, -//CHECK-SAME: %[[A1:[0-9a-zA-Z_\.]+]]: !felt.type) -> !struct.type<@AddrDecomposeBits> attributes {function.allow_witness} { +//CHECK-SAME: %[[A1:[0-9a-zA-Z_\.]+]]: !felt.type) -> !struct.type<@AddrDecomposeBits> attributes {function.allow_non_native_field_ops, function.allow_witness} { //CHECK-NEXT: %[[SELF:[0-9a-zA-Z_\.]+]] = struct.new : <@AddrDecomposeBits> //CHECK-NEXT: %[[T00:[0-9a-zA-Z_\.]+]] = struct.readf %[[A0]][@low] : <@std::@risc0::@ValU32>, !felt.type //CHECK-NEXT: %[[C1:[0-9a-zA-Z_\.]+]] = felt.const 1 diff --git a/test/FrontendLang/Zirgen/zir_example_9.llzk b/test/FrontendLang/Zirgen/zir_example_9.llzk index b3b71a6cc..81d015660 100644 --- a/test/FrontendLang/Zirgen/zir_example_9.llzk +++ b/test/FrontendLang/Zirgen/zir_example_9.llzk @@ -1,4 +1,4 @@ -// RUN: llzk-opt -split-input-file -verify-diagnostics %s | FileCheck --enable-var-scope %s +// RUN: llzk-opt -verify-diagnostics %s | FileCheck --enable-var-scope %s #map = affine_map<()[s0, s1] -> (s0 + s1)> module attributes {veridise.lang = "llzk"} { @@ -35,7 +35,7 @@ module attributes {veridise.lang = "llzk"} { // ZIR frontend should mark function.return value with `pub` struct.field @synthetic_return : !felt.type {llzk.pub} - function.def @compute(%lhs: !felt.type, %rhs: !felt.type) -> !struct.type<@Div<[]>> { + function.def @compute(%lhs: !felt.type, %rhs: !felt.type) -> !struct.type<@Div<[]>> attributes {function.allow_non_native_field_ops} { %self = struct.new : !struct.type<@Div<[]>> // res_inv := inv(rhs); %res_inv = felt.inv %rhs @@ -66,7 +66,7 @@ module attributes {veridise.lang = "llzk"} { struct.field @"$super" : !struct.type<@Component<[]>> struct.field @"$temp_0" : !struct.type<@Component<[]>> struct.field @"$temp" : !struct.type<@Div<[]>> - function.def @compute(%arg0: !array.type<@Aff$0 x !felt.type>) -> !struct.type<@Foo<[@N, @P, @Aff$0]>> { + function.def @compute(%arg0: !array.type<@Aff$0 x !felt.type>) -> !struct.type<@Foo<[@N, @P, @Aff$0]>> attributes {function.allow_non_native_field_ops} { %self = struct.new : !struct.type<@Foo<[@N, @P, @Aff$0]>> %0 = poly.read_const @N : !felt.type %1 = poly.read_const @P : !felt.type @@ -95,7 +95,7 @@ module attributes {veridise.lang = "llzk"} { struct.field @"$temp_1" : !struct.type<@Component<[]>> struct.field @"$temp_0" : !struct.type<@Foo<[@N, @P, #map]>> struct.field @"$temp" : !struct.type<@Div<[]>> - function.def @compute(%arg0: !array.type<@Aff$0 x !felt.type>) -> !struct.type<@Bar<[@N, @P, @Aff$0]>> { + function.def @compute(%arg0: !array.type<@Aff$0 x !felt.type>) -> !struct.type<@Bar<[@N, @P, @Aff$0]>> attributes {function.allow_non_native_field_ops} { %self = struct.new : !struct.type<@Bar<[@N, @P, @Aff$0]>> %0 = poly.read_const @N : !felt.type %1 = poly.read_const @P : !felt.type @@ -158,7 +158,7 @@ module attributes {veridise.lang = "llzk"} { // CHECK-LABEL: struct.def @Div<[]> { // CHECK-NEXT: struct.field @reciprocal : !felt.type // CHECK-NEXT: struct.field @synthetic_return : !felt.type {llzk.pub} -// CHECK-NEXT: function.def @compute(%[[V0:[0-9a-zA-Z_\.]+]]: !felt.type, %[[V1:[0-9a-zA-Z_\.]+]]: !felt.type) -> !struct.type<@Div<[]>> attributes {function.allow_witness} { +// CHECK-NEXT: function.def @compute(%[[V0:[0-9a-zA-Z_\.]+]]: !felt.type, %[[V1:[0-9a-zA-Z_\.]+]]: !felt.type) -> !struct.type<@Div<[]>> attributes {function.allow_non_native_field_ops, function.allow_witness} { // CHECK-NEXT: %[[V2:[0-9a-zA-Z_\.]+]] = struct.new : <@Div<[]>> // CHECK-NEXT: %[[V3:[0-9a-zA-Z_\.]+]] = felt.inv %[[V1]] : !felt.type // CHECK-NEXT: struct.writef %[[V2]][@reciprocal] = %[[V3]] : <@Div<[]>>, !felt.type @@ -182,7 +182,7 @@ module attributes {veridise.lang = "llzk"} { // CHECK-NEXT: struct.field @"$super" : !struct.type<@Component<[]>> // CHECK-NEXT: struct.field @"$temp_0" : !struct.type<@Component<[]>> // CHECK-NEXT: struct.field @"$temp" : !struct.type<@Div<[]>> -// CHECK-NEXT: function.def @compute(%[[V0:[0-9a-zA-Z_\.]+]]: !array.type<@Aff$0 x !felt.type>) -> !struct.type<@Foo<[@N, @P, @Aff$0]>> attributes {function.allow_witness} { +// CHECK-NEXT: function.def @compute(%[[V0:[0-9a-zA-Z_\.]+]]: !array.type<@Aff$0 x !felt.type>) -> !struct.type<@Foo<[@N, @P, @Aff$0]>> attributes {function.allow_non_native_field_ops, function.allow_witness} { // CHECK-NEXT: %[[V1:[0-9a-zA-Z_\.]+]] = struct.new : <@Foo<[@N, @P, @Aff$0]>> // CHECK-NEXT: %[[V2:[0-9a-zA-Z_\.]+]] = poly.read_const @N : !felt.type // CHECK-NEXT: %[[V3:[0-9a-zA-Z_\.]+]] = poly.read_const @P : !felt.type @@ -211,7 +211,7 @@ module attributes {veridise.lang = "llzk"} { // CHECK-NEXT: struct.field @"$temp_1" : !struct.type<@Component<[]>> // CHECK-NEXT: struct.field @"$temp_0" : !struct.type<@Foo<[@N, @P, #[[$M0]]]>> // CHECK-NEXT: struct.field @"$temp" : !struct.type<@Div<[]>> -// CHECK-NEXT: function.def @compute(%[[V0:[0-9a-zA-Z_\.]+]]: !array.type<@Aff$0 x !felt.type>) -> !struct.type<@Bar<[@N, @P, @Aff$0]>> attributes {function.allow_witness} { +// CHECK-NEXT: function.def @compute(%[[V0:[0-9a-zA-Z_\.]+]]: !array.type<@Aff$0 x !felt.type>) -> !struct.type<@Bar<[@N, @P, @Aff$0]>> attributes {function.allow_non_native_field_ops, function.allow_witness} { // CHECK-NEXT: %[[V1:[0-9a-zA-Z_\.]+]] = struct.new : <@Bar<[@N, @P, @Aff$0]>> // CHECK-NEXT: %[[V2:[0-9a-zA-Z_\.]+]] = poly.read_const @N : !felt.type // CHECK-NEXT: %[[V3:[0-9a-zA-Z_\.]+]] = poly.read_const @P : !felt.type diff --git a/test/Inputs/bits.llzk b/test/Inputs/bits.llzk index b1326dec4..77025486c 100644 --- a/test/Inputs/bits.llzk +++ b/test/Inputs/bits.llzk @@ -36,7 +36,7 @@ module attributes {veridise.lang = "llzk"} { } struct.def @EqzExt<[]> { struct.field @"$super" : !struct.type<@Component<[]>> {llzk.pub} - function.def @compute(%arg0: !array.type<4 x !felt.type>) -> !struct.type<@EqzExt<[]>> { + function.def @compute(%arg0: !array.type<4 x !felt.type>) -> !struct.type<@EqzExt<[]>> attributes {function.allow_non_native_field_ops} { %self = struct.new : <@EqzExt<[]>> %c0 = arith.constant 0 : index %0 = array.read %arg0[%c0] : <4 x !felt.type>, !felt.type @@ -90,7 +90,7 @@ module attributes {veridise.lang = "llzk"} { struct.field @"$super" : !struct.type<@NondetExtReg<[]>> struct.field @"$temp" : !struct.type<@EqzExt<[]>> struct.field @reg : !struct.type<@NondetExtReg<[]>> - function.def @compute(%arg0: !array.type<4 x !felt.type>) -> !struct.type<@ExtReg<[]>> { + function.def @compute(%arg0: !array.type<4 x !felt.type>) -> !struct.type<@ExtReg<[]>> attributes {function.allow_non_native_field_ops} { %self = struct.new : <@ExtReg<[]>> %0 = function.call @NondetExtReg::@compute(%arg0) : (!array.type<4 x !felt.type>) -> !struct.type<@NondetExtReg<[]>> struct.writef %self[@reg] = %0 : <@ExtReg<[]>>, !struct.type<@NondetExtReg<[]>> @@ -156,7 +156,7 @@ module attributes {veridise.lang = "llzk"} { struct.def @Div<[]> { struct.field @"$super" : !felt.type {llzk.pub} struct.field @reciprocal : !felt.type - function.def @compute(%arg0: !felt.type, %arg1: !felt.type) -> !struct.type<@Div<[]>> { + function.def @compute(%arg0: !felt.type, %arg1: !felt.type) -> !struct.type<@Div<[]>> attributes {function.allow_non_native_field_ops} { %self = struct.new : <@Div<[]>> %0 = felt.inv %arg1 : !felt.type struct.writef %self[@reciprocal] = %0 : <@Div<[]>>, !felt.type @@ -411,7 +411,7 @@ module attributes {veridise.lang = "llzk"} { struct.field @"$temp_0" : !struct.type<@BitAnd<[]>> struct.field @reg0 : !struct.type<@NondetBitReg<[]>> struct.field @"$temp" : !struct.type<@BitAnd<[]>> - function.def @compute(%arg0: !felt.type) -> !struct.type<@NondetFakeTwitReg<[]>> { + function.def @compute(%arg0: !felt.type) -> !struct.type<@NondetFakeTwitReg<[]>> attributes {function.allow_non_native_field_ops} { %self = struct.new : <@NondetFakeTwitReg<[]>> %felt_const_1 = felt.const 1 %0 = function.call @BitAnd::@compute(%arg0, %felt_const_1) : (!felt.type, !felt.type) -> !struct.type<@BitAnd<[]>> @@ -504,7 +504,7 @@ module attributes {veridise.lang = "llzk"} { struct.def @FakeTwitReg<[]> { struct.field @"$super" : !struct.type<@NondetFakeTwitReg<[]>> struct.field @reg : !struct.type<@NondetFakeTwitReg<[]>> - function.def @compute(%arg0: !felt.type) -> !struct.type<@FakeTwitReg<[]>> { + function.def @compute(%arg0: !felt.type) -> !struct.type<@FakeTwitReg<[]>> attributes {function.allow_non_native_field_ops} { %self = struct.new : <@FakeTwitReg<[]>> %0 = function.call @NondetFakeTwitReg::@compute(%arg0) : (!felt.type) -> !struct.type<@NondetFakeTwitReg<[]>> struct.writef %self[@reg] = %0 : <@FakeTwitReg<[]>>, !struct.type<@NondetFakeTwitReg<[]>> diff --git a/test/Transforms/Flattening/mastermind_with_main.llzk b/test/Transforms/Flattening/mastermind_with_main.llzk index 4946ed2fa..274ba3168 100644 --- a/test/Transforms/Flattening/mastermind_with_main.llzk +++ b/test/Transforms/Flattening/mastermind_with_main.llzk @@ -39,7 +39,7 @@ module attributes {veridise.lang = "llzk"} { } struct.def @EqzExt<[]> { struct.field @"$super" : !struct.type<@Component<[]>> - function.def @compute(%arg0: !array.type<4 x !felt.type>) -> !struct.type<@EqzExt<[]>> attributes {function.allow_witness} { + function.def @compute(%arg0: !array.type<4 x !felt.type>) -> !struct.type<@EqzExt<[]>> attributes {function.allow_non_native_field_ops, function.allow_witness} { %felt_const_0 = felt.const 0 %c3 = arith.constant 3 : index %c2 = arith.constant 2 : index @@ -90,7 +90,7 @@ module attributes {veridise.lang = "llzk"} { struct.field @"$super" : !struct.type<@NondetExtReg<[]>> struct.field @"$temp" : !struct.type<@EqzExt<[]>> struct.field @reg : !struct.type<@NondetExtReg<[]>> {column} - function.def @compute(%arg0: !array.type<4 x !felt.type>) -> !struct.type<@ExtReg<[]>> attributes {function.allow_witness} { + function.def @compute(%arg0: !array.type<4 x !felt.type>) -> !struct.type<@ExtReg<[]>> attributes {function.allow_non_native_field_ops, function.allow_witness} { %c3 = arith.constant 3 : index %c2 = arith.constant 2 : index %c1 = arith.constant 1 : index @@ -148,7 +148,7 @@ module attributes {veridise.lang = "llzk"} { struct.def @Div<[]> { struct.field @"$super" : !felt.type struct.field @reciprocal : !felt.type - function.def @compute(%arg0: !felt.type, %arg1: !felt.type) -> !struct.type<@Div<[]>> attributes {function.allow_witness} { + function.def @compute(%arg0: !felt.type, %arg1: !felt.type) -> !struct.type<@Div<[]>> attributes {function.allow_non_native_field_ops, function.allow_witness} { %self = struct.new : !struct.type<@Div<[]>> %0 = felt.inv %arg1 : !felt.type struct.writef %self[@reciprocal] = %0 : <@Div<[]>>, !felt.type @@ -2000,7 +2000,7 @@ module attributes {veridise.lang = "llzk"} { struct.field @inv : !struct.type<@NondetReg<[]>> {column} struct.field @"$temp" : !felt.type struct.field @isZero : !struct.type<@NondetReg<[]>> {column} - function.def @compute(%arg0: !felt.type) -> !struct.type<@IsZero<[]>> attributes {function.allow_witness} { + function.def @compute(%arg0: !felt.type) -> !struct.type<@IsZero<[]>> attributes {function.allow_non_native_field_ops, function.allow_witness} { %felt_const_0 = felt.const 0 %self = struct.new : !struct.type<@IsZero<[]>> %0 = bool.cmp eq(%arg0, %felt_const_0) @@ -2057,7 +2057,7 @@ module attributes {veridise.lang = "llzk"} { struct.def @Eq<[]> { struct.field @"$super" : !struct.type<@IsZero<[]>> {llzk.pub} struct.field @"$temp" : !struct.type<@IsZero<[]>> {column} - function.def @compute(%arg0: !felt.type, %arg1: !felt.type) -> !struct.type<@Eq<[]>> attributes {function.allow_witness} { + function.def @compute(%arg0: !felt.type, %arg1: !felt.type) -> !struct.type<@Eq<[]>> attributes {function.allow_non_native_field_ops, function.allow_witness} { %self = struct.new : !struct.type<@Eq<[]>> %0 = felt.sub %arg0, %arg1 : !felt.type, !felt.type %1 = function.call @IsZero::@compute(%0) : (!felt.type) -> !struct.type<@IsZero<[]>> @@ -2077,7 +2077,7 @@ module attributes {veridise.lang = "llzk"} { struct.field @"$super" : !struct.type<@Eq<[]>> struct.field @"$temp" : !struct.type<@Assert<[]>> struct.field @r : !struct.type<@Eq<[]>> {column} - function.def @compute(%arg0: !poly.tvar<@T>, %arg1: !poly.tvar<@T>) -> !struct.type<@EnsureEq<[@T]>> attributes {function.allow_witness} { + function.def @compute(%arg0: !poly.tvar<@T>, %arg1: !poly.tvar<@T>) -> !struct.type<@EnsureEq<[@T]>> attributes {function.allow_non_native_field_ops, function.allow_witness} { %0 = string.new "Provided values are not equal" %felt_const_0 = felt.const 0 %self = struct.new : !struct.type<@EnsureEq<[@T]>> @@ -2721,7 +2721,7 @@ module attributes {veridise.lang = "llzk"} { struct.field @"$temp_0" : !array.type<@N x !felt.type> struct.field @"$temp" : !array.type<@N x !struct.type<@IsZero<[]>>> {column} struct.field @"$array" : !array.type<@N x !struct.type<@IsZero<[]>>> {column} - function.def @compute(%arg0: !struct.type<@Pegs<[@N]>>, %arg1: !felt.type) -> !struct.type<@CountColors<[@N]>> attributes {function.allow_witness} { + function.def @compute(%arg0: !struct.type<@Pegs<[@N]>>, %arg1: !felt.type) -> !struct.type<@CountColors<[@N]>> attributes {function.allow_non_native_field_ops, function.allow_witness} { %felt_const_0 = felt.const 0 %c0 = arith.constant 0 : index %c1 = arith.constant 1 : index @@ -2907,7 +2907,7 @@ module attributes {veridise.lang = "llzk"} { struct.field @"$temp_0" : !array.type<#map x !struct.type<@EnsureEq<[!poly.tvar<@T>]>>> {column} struct.field @"$array" : !array.type<#map x !struct.type<@Component<[]>>> struct.field @"$temp" : !struct.type<@Zip<[!poly.tvar<@T>, !poly.tvar<@T>, @N]>> - function.def @compute(%arg0: !array.type<@N x !poly.tvar<@T>>, %arg1: !array.type<@N x !poly.tvar<@T>>) -> !struct.type<@AssertArrsEq<[@T, @N]>> attributes {function.allow_witness} { + function.def @compute(%arg0: !array.type<@N x !poly.tvar<@T>>, %arg1: !array.type<@N x !poly.tvar<@T>>) -> !struct.type<@AssertArrsEq<[@T, @N]>> attributes {function.allow_non_native_field_ops, function.allow_witness} { %c0 = arith.constant 0 : index %c1 = arith.constant 1 : index %self = struct.new : !struct.type<@AssertArrsEq<[@T, @N]>> @@ -2991,7 +2991,7 @@ module attributes {veridise.lang = "llzk"} { struct.field @"$temp_0" : !struct.type<@AssertArrsEq<[!felt.type, 24]>> struct.field @code : !struct.type<@SetCode<[@COLORS, @PEGS]>> struct.field @"$temp" : !struct.type<@CheckBounds<[@COLORS, @PEGS]>> - function.def @compute(%arg0: !struct.type<@Nonce<[]>>, %arg1: !struct.type<@Pegs<[@PEGS]>>, %arg2: !struct.type<@CodeHash<[]>>, %arg3: !struct.type<@Pegs<[@PEGS]>>) -> !struct.type<@MakeGuess<[@COLORS, @PEGS]>> attributes {function.allow_witness} { + function.def @compute(%arg0: !struct.type<@Nonce<[]>>, %arg1: !struct.type<@Pegs<[@PEGS]>>, %arg2: !struct.type<@CodeHash<[]>>, %arg3: !struct.type<@Pegs<[@PEGS]>>) -> !struct.type<@MakeGuess<[@COLORS, @PEGS]>> attributes {function.allow_non_native_field_ops, function.allow_witness} { %0 = string.new "Partial guesses: %u" %1 = string.new "Correct guesses: %u" %felt_const_0 = felt.const 0 @@ -3270,7 +3270,7 @@ module attributes {veridise.lang = "llzk"} { struct.field @"$super" : !struct.type<@MakeGuess<[@COLORS, @PEGS]>> {llzk.pub} struct.field @"$temp" : !struct.type<@Assert<[]>> struct.field @guess : !struct.type<@MakeGuess<[@COLORS, @PEGS]>> {column} - function.def @compute(%arg0: !struct.type<@Nonce<[]>>, %arg1: !struct.type<@Pegs<[@PEGS]>>, %arg2: !struct.type<@CodeHash<[]>>, %arg3: !struct.type<@Pegs<[@PEGS]>>) -> !struct.type<@MakeGuessWithChecks<[@COLORS, @PEGS]>> attributes {function.allow_witness} { + function.def @compute(%arg0: !struct.type<@Nonce<[]>>, %arg1: !struct.type<@Pegs<[@PEGS]>>, %arg2: !struct.type<@CodeHash<[]>>, %arg3: !struct.type<@Pegs<[@PEGS]>>) -> !struct.type<@MakeGuessWithChecks<[@COLORS, @PEGS]>> attributes {function.allow_non_native_field_ops, function.allow_witness} { %0 = string.new "Guess check post condition failed" %felt_const_1 = felt.const 1 %felt_const_0 = felt.const 0 @@ -3398,7 +3398,7 @@ module attributes {veridise.lang = "llzk"} { struct.field @codeHash : !struct.type<@SetCode<[6, 4]>> struct.field @codemakerCode : !struct.type<@Pegs<[4]>> {column} struct.field @codemakerNonce : !struct.type<@Nonce<[]>> {column} - function.def @compute() -> !struct.type<@Main<[]>> attributes {function.allow_witness} { + function.def @compute() -> !struct.type<@Main<[]>> attributes {function.allow_non_native_field_ops, function.allow_witness} { %felt_const_3 = felt.const 3 %felt_const_4 = felt.const 4 %felt_const_1 = felt.const 1 diff --git a/test/Transforms/Flattening/zir_example_9.llzk b/test/Transforms/Flattening/zir_example_9.llzk index c99dc96b0..810601ef6 100644 --- a/test/Transforms/Flattening/zir_example_9.llzk +++ b/test/Transforms/Flattening/zir_example_9.llzk @@ -35,7 +35,7 @@ module attributes {veridise.lang = "llzk"} { // ZIR frontend should mark function.return value with `pub` struct.field @synthetic_return : !felt.type {llzk.pub} - function.def @compute(%lhs: !felt.type, %rhs: !felt.type) -> !struct.type<@Div<[]>> { + function.def @compute(%lhs: !felt.type, %rhs: !felt.type) -> !struct.type<@Div<[]>> attributes {function.allow_non_native_field_ops} { %self = struct.new : !struct.type<@Div<[]>> // res_inv := inv(rhs); %res_inv = felt.inv %rhs @@ -66,7 +66,7 @@ module attributes {veridise.lang = "llzk"} { struct.field @"$super" : !struct.type<@Component<[]>> struct.field @"$temp_0" : !struct.type<@Component<[]>> struct.field @"$temp" : !struct.type<@Div<[]>> - function.def @compute(%arg0: !array.type<@Aff$0 x !felt.type>) -> !struct.type<@Foo<[@N, @P, @Aff$0]>> { + function.def @compute(%arg0: !array.type<@Aff$0 x !felt.type>) -> !struct.type<@Foo<[@N, @P, @Aff$0]>> attributes {function.allow_non_native_field_ops} { %self = struct.new : !struct.type<@Foo<[@N, @P, @Aff$0]>> %0 = poly.read_const @N : !felt.type %1 = poly.read_const @P : !felt.type @@ -95,7 +95,7 @@ module attributes {veridise.lang = "llzk"} { struct.field @"$temp_1" : !struct.type<@Component<[]>> struct.field @"$temp_0" : !struct.type<@Foo<[@N, @P, #map]>> struct.field @"$temp" : !struct.type<@Div<[]>> - function.def @compute(%arg0: !array.type<@Aff$0 x !felt.type>) -> !struct.type<@Bar<[@N, @P, @Aff$0]>> { + function.def @compute(%arg0: !array.type<@Aff$0 x !felt.type>) -> !struct.type<@Bar<[@N, @P, @Aff$0]>> attributes {function.allow_non_native_field_ops} { %self = struct.new : !struct.type<@Bar<[@N, @P, @Aff$0]>> %0 = poly.read_const @N : !felt.type %1 = poly.read_const @P : !felt.type @@ -127,7 +127,7 @@ module attributes {veridise.lang = "llzk"} { } struct.def @Main { - function.def @compute() -> !struct.type<@Main> { + function.def @compute() -> !struct.type<@Main> attributes {function.allow_non_native_field_ops} { %self = struct.new : !struct.type<@Main> %5 = arith.constant 5 : index %2 = arith.constant 2 : index @@ -167,7 +167,7 @@ module attributes {veridise.lang = "llzk"} { // CHECK-LABEL: struct.def @Div { // CHECK-NEXT: struct.field @reciprocal : !felt.type // CHECK-NEXT: struct.field @synthetic_return : !felt.type {llzk.pub} -// CHECK-NEXT: function.def @compute(%[[V0:[0-9a-zA-Z_\.]+]]: !felt.type, %[[V1:[0-9a-zA-Z_\.]+]]: !felt.type) -> !struct.type<@Div> attributes {function.allow_witness} { +// CHECK-NEXT: function.def @compute(%[[V0:[0-9a-zA-Z_\.]+]]: !felt.type, %[[V1:[0-9a-zA-Z_\.]+]]: !felt.type) -> !struct.type<@Div> attributes {function.allow_non_native_field_ops, function.allow_witness} { // CHECK-NEXT: %[[V2:[0-9a-zA-Z_\.]+]] = struct.new : <@Div> // CHECK-NEXT: %[[V3:[0-9a-zA-Z_\.]+]] = felt.inv %[[V1]] : !felt.type // CHECK-NEXT: struct.writef %[[V2]][@reciprocal] = %[[V3]] : <@Div>, !felt.type @@ -191,7 +191,7 @@ module attributes {veridise.lang = "llzk"} { // CHECK-NEXT: struct.field @"$super" : !struct.type<@Component> // CHECK-NEXT: struct.field @"$temp_0" : !struct.type<@Component> // CHECK-NEXT: struct.field @"$temp" : !struct.type<@Div> -// CHECK-NEXT: function.def @compute(%[[V0:[0-9a-zA-Z_\.]+]]: !array.type<7 x !felt.type>) -> !struct.type<@Foo_4_3_7> attributes {function.allow_witness} { +// CHECK-NEXT: function.def @compute(%[[V0:[0-9a-zA-Z_\.]+]]: !array.type<7 x !felt.type>) -> !struct.type<@Foo_4_3_7> attributes {function.allow_non_native_field_ops, function.allow_witness} { // CHECK-NEXT: %[[V1:[0-9a-zA-Z_\.]+]] = felt.const 3 // CHECK-NEXT: %[[V2:[0-9a-zA-Z_\.]+]] = felt.const 4 // CHECK-NEXT: %[[V3:[0-9a-zA-Z_\.]+]] = struct.new : <@Foo_4_3_7> @@ -220,7 +220,7 @@ module attributes {veridise.lang = "llzk"} { // CHECK-NEXT: struct.field @"$temp_1" : !struct.type<@Component> // CHECK-NEXT: struct.field @"$temp_0" : !struct.type<@Foo_4_3_7> // CHECK-NEXT: struct.field @"$temp" : !struct.type<@Div> -// CHECK-NEXT: function.def @compute(%[[V0:[0-9a-zA-Z_\.]+]]: !array.type<7 x !felt.type>) -> !struct.type<@Bar_4_3_7> attributes {function.allow_witness} { +// CHECK-NEXT: function.def @compute(%[[V0:[0-9a-zA-Z_\.]+]]: !array.type<7 x !felt.type>) -> !struct.type<@Bar_4_3_7> attributes {function.allow_non_native_field_ops, function.allow_witness} { // CHECK-NEXT: %[[V1:[0-9a-zA-Z_\.]+]] = felt.const 3 // CHECK-NEXT: %[[V2:[0-9a-zA-Z_\.]+]] = felt.const 4 // CHECK-NEXT: %[[V3:[0-9a-zA-Z_\.]+]] = struct.new : <@Bar_4_3_7> @@ -250,7 +250,7 @@ module attributes {veridise.lang = "llzk"} { // CHECK-NEXT: } // // CHECK-LABEL: struct.def @Main { -// CHECK-NEXT: function.def @compute() -> !struct.type<@Main> attributes {function.allow_witness} { +// CHECK-NEXT: function.def @compute() -> !struct.type<@Main> attributes {function.allow_non_native_field_ops, function.allow_witness} { // CHECK-NEXT: %[[V0:[0-9a-zA-Z_\.]+]] = struct.new : <@Main> // CHECK-NEXT: %[[V1:[0-9a-zA-Z_\.]+]] = array.new : <7 x !felt.type> // CHECK-NEXT: %[[V2:[0-9a-zA-Z_\.]+]] = function.call @Bar_4_3_7::@compute(%[[V1]]) : (!array.type<7 x !felt.type>) -> !struct.type<@Bar_4_3_7> diff --git a/test/Transforms/RedundantAndUnusedElim/redundant_op_pass.llzk b/test/Transforms/RedundantAndUnusedElim/redundant_op_pass.llzk index b31d59be6..8738d3797 100644 --- a/test/Transforms/RedundantAndUnusedElim/redundant_op_pass.llzk +++ b/test/Transforms/RedundantAndUnusedElim/redundant_op_pass.llzk @@ -141,7 +141,7 @@ module attributes {veridise.lang = "llzk"} { // CHECK-NEXT: struct.def @Div { // CHECK-NEXT: struct.field @reciprocal : !felt.type // CHECK-NEXT: struct.field @synthetic_return : !felt.type {llzk.pub} -// CHECK-NEXT: function.def @compute(%[[VAL_11:.*]]: !felt.type, %[[VAL_12:.*]]: !felt.type) -> !struct.type<@risc0::@Div> attributes {function.allow_witness} { +// CHECK-NEXT: function.def @compute(%[[VAL_11:.*]]: !felt.type, %[[VAL_12:.*]]: !felt.type) -> !struct.type<@risc0::@Div> attributes {function.allow_non_native_field_ops, function.allow_witness} { // CHECK-NEXT: %[[VAL_13:.*]] = struct.new : <@risc0::@Div> // CHECK-NEXT: %[[VAL_14:.*]] = felt.inv %[[VAL_12]] : !felt.type // CHECK-NEXT: struct.writef %[[VAL_13]][@reciprocal] = %[[VAL_14]] : <@risc0::@Div>, !felt.type diff --git a/unittests/CAPI/Dialect/Function.cpp b/unittests/CAPI/Dialect/Function.cpp index c6c196484..bd1eedbcf 100644 --- a/unittests/CAPI/Dialect/Function.cpp +++ b/unittests/CAPI/Dialect/Function.cpp @@ -138,6 +138,20 @@ TEST_F(FuncDialectTest, llzk_func_def_op_set_allow_witness_attr) { EXPECT_TRUE(!llzkFuncDefOpGetHasAllowWitnessAttr(f.op)); } +TEST_F(FuncDialectTest, llzk_func_def_op_get_has_allow_non_native_field_ops_attr) { + auto f = test_function(); + EXPECT_TRUE(!llzkFuncDefOpGetHasAllowNonNativeFieldOpsAttr(f.op)); +} + +TEST_F(FuncDialectTest, llzk_func_def_op_set_allow_non_native_field_ops_attr) { + auto f = test_function(); + EXPECT_TRUE(!llzkFuncDefOpGetHasAllowNonNativeFieldOpsAttr(f.op)); + llzkFuncDefOpSetAllowNonNativeFieldOpsAttr(f.op, true); + EXPECT_TRUE(llzkFuncDefOpGetHasAllowNonNativeFieldOpsAttr(f.op)); + llzkFuncDefOpSetAllowNonNativeFieldOpsAttr(f.op, false); + EXPECT_TRUE(!llzkFuncDefOpGetHasAllowNonNativeFieldOpsAttr(f.op)); +} + TEST_F(FuncDialectTest, llzk_func_def_op_get_has_arg_is_pub) { auto f = test_function(); EXPECT_TRUE(!llzkFuncDefOpGetHasArgIsPub(f.op, 0));