remove remaining uses of "Signal"

changelogs/unreleased/th__cleanup_signal_comments.yaml

@@ -0,0 +1,3 @@
+fixed:
+  - "outdated documentation"
+  - "restrict `cast.toindex` to functions with `allow_non_native_field_ops` attribute"

include/llzk/Dialect/Cast/IR/Ops.h

@@ -11,6 +11,7 @@
 
 #include "llzk/Dialect/Cast/IR/Dialect.h"
 #include "llzk/Dialect/Felt/IR/Types.h"
+#include "llzk/Dialect/Function/IR/OpTraits.h"
 
 // Include TableGen'd declarations
 #define GET_OP_CLASSES

include/llzk/Dialect/Cast/IR/Ops.td

@@ -13,6 +13,7 @@
 include "llzk/Dialect/Shared/Types.td"
 include "llzk/Dialect/Cast/IR/Dialect.td"
 include "llzk/Dialect/Felt/IR/Types.td"
+include "llzk/Dialect/Function/IR/OpTraits.td"
 
 include "mlir/IR/OpBase.td"
 include "mlir/Interfaces/SideEffectInterfaces.td"
@@ -36,12 +37,11 @@ def LLZK_IntToFeltOp : Op<CastDialect, "tofelt", [Pure]> {
   let assemblyFormat = [{ $value `:` type($value) attr-dict }];
 }
 
-def LLZK_FeltToIndexOp : Op<CastDialect, "toindex", [Pure]> {
+def LLZK_FeltToIndexOp : Op<CastDialect, "toindex", [Pure, NotFieldNative]> {
   let summary = "convert a field element into an index";
   let description = [{
-    This operation converts a field element value into an index value to allow
-    use as an array index or loop bound. In struct @constrain functions, the
-    argument to this op is not allowed to be derived from a Signal struct.
+    This operation converts a field element value into an index value to allow use
+    as an array index or loop bound.
 
     Example:
     ```llzk
@@ -53,8 +53,6 @@ def LLZK_FeltToIndexOp : Op<CastDialect, "toindex", [Pure]> {
   let arguments = (ins LLZK_FeltType:$value);
   let results = (outs Index:$result);
   let assemblyFormat = [{ $value attr-dict }];
-
-  let hasVerifier = 1;
 }
 
 #endif // LLZK_CAST_OPS

include/llzk/Dialect/Shared/Types.td

@@ -18,9 +18,8 @@ def AnyLLZKType : Type<CPred<"::llzk::isValidType($_self)">,
 def GlobalDefType : Type<CPred<"::llzk::isValidGlobalType($_self)">,
                          "any LLZK type except non-constant types">;
 
-def EmitEqType
-    : Type<CPred<"::llzk::isValidEmitEqType($_self)">,
-           "any LLZK type, excluding non-Signal struct and string types">;
+def EmitEqType : Type<CPred<"::llzk::isValidEmitEqType($_self)">,
+                      "any LLZK type, excluding struct and string types">;
 
 def ConstReadType : Type<CPred<"::llzk::isValidConstReadType($_self)">,
                          "integral, felt, or typevar type">;

lib/Analysis/IntervalAnalysis.cpp

@@ -577,7 +577,7 @@ mlir::LogicalResult IntervalDataFlowAnalysis::visitOperation(
     }
   } else if (
       // We do not need to explicitly handle read ops since they are resolved at the operand value
-      // step where `SourceRef`s are queries (with the exception of the Signal struct, see above).
+      // step where `SourceRef`s are queries.
       !isReadOp(op)
       // We do not currently handle return ops as the analysis is currently limited to constrain
       // functions, which return no value.

lib/Dialect/Cast/IR/Ops.cpp

@@ -14,39 +14,3 @@
 // TableGen'd implementation files
 #define GET_OP_CLASSES
 #include "llzk/Dialect/Cast/IR/Ops.cpp.inc"
-
-using namespace mlir;
-using namespace llzk::component;
-using namespace llzk::function;
-
-namespace llzk::cast {
-
-//===------------------------------------------------------------------===//
-// FeltToIndexOp
-//===------------------------------------------------------------------===//
-
-LogicalResult FeltToIndexOp::verify() {
-  if (auto parentOr = getParentOfType<FuncDefOp>(*this);
-      succeeded(parentOr) && !parentOr->hasAllowWitnessAttr()) {
-    // Traverse the def-use chain to see if this operand, which is a felt, ever
-    // derives from a Signal struct.
-    SmallVector<Value, 2> frontier {getValue()};
-    DenseSet<Value> visited;
-
-    while (!frontier.empty()) {
-      Value v = frontier.pop_back_val();
-      if (visited.contains(v)) {
-        continue;
-      }
-      visited.insert(v);
-
-      if (Operation *op = v.getDefiningOp()) {
-        frontier.insert(frontier.end(), op->operand_begin(), op->operand_end());
-      }
-    }
-  }
-
-  return success();
-}
-
-} // namespace llzk::cast

lib/Dialect/Constrain/IR/Ops.cpp

@@ -60,9 +60,7 @@ LogicalResult EmitContainmentOp::verify() {
   Type elemTy = arrType.getElementType();
   if (!isValidEmitEqType(elemTy)) {
     return errFn().append(
-        "element type must be any LLZK type, excluding non-Signal struct and string types, but "
-        "got ",
-        elemTy
+        "element type must be any LLZK type, excluding struct and string types, but got ", elemTy
     );
   }
   return success();

test/Analysis/constraint_dependency_graph_pass.llzk

@@ -766,7 +766,7 @@ module attributes {llzk.lang} {
     struct.member @outp : !array.type<#map x !felt.type> {column}
     struct.member @"$temp" : !array.type<#map x !felt.type> {column}
     struct.member @internal : !array.type<#map x !felt.type> {column}
-    function.def @compute(%arg0: !array.type<@N x !felt.type>) -> !struct.type<@Foo<[@N]>> attributes {function.allow_witness} {
+    function.def @compute(%arg0: !array.type<@N x !felt.type>) -> !struct.type<@Foo<[@N]>> attributes {function.allow_witness, function.allow_non_native_field_ops} {
       %c0 = arith.constant 0 : index
       %c1 = arith.constant 1 : index
       %self = struct.new : <@Foo<[@N]>>
@@ -817,7 +817,7 @@ module attributes {llzk.lang} {
       struct.writem %self[@outp] = %array_2 : <@Foo<[@N]>>, !array.type<#map x !felt.type>
       function.return %self : !struct.type<@Foo<[@N]>>
     }
-    function.def @constrain(%arg0: !struct.type<@Foo<[@N]>>,  %arg1: !array.type<@N x !felt.type>) attributes {function.allow_constraint} {
+    function.def @constrain(%arg0: !struct.type<@Foo<[@N]>>,  %arg1: !array.type<@N x !felt.type>) attributes {function.allow_constraint, function.allow_non_native_field_ops} {
       %c0 = arith.constant 0 : index
       %c1 = arith.constant 1 : index
       %0 = poly.read_const @N : !felt.type

test/Analysis/interval_analysis/edwards2montgomery.llzk

@@ -264,7 +264,7 @@ module attributes {llzk.lang} {
       struct.writem %self[@"$super"] = %array : <@Edwards2Montgomery<[]>>, !array.type<2 x !struct.type<@NondetReg<[]>>>
       function.return %self : !struct.type<@Edwards2Montgomery<[]>>
     }
-    function.def @constrain(%arg0: !struct.type<@Edwards2Montgomery<[]>>, %arg1: !array.type<2 x !felt.type>) attributes {function.allow_constraint} {
+    function.def @constrain(%arg0: !struct.type<@Edwards2Montgomery<[]>>, %arg1: !array.type<2 x !felt.type>) attributes {function.allow_non_native_field_ops, function.allow_constraint} {
       %felt_const_0 = felt.const  0
       %felt_const_1 = felt.const  1
       %0 = cast.toindex %felt_const_1

test/Dialect/Cast/type_convert_fail.llzk

@@ -91,3 +91,20 @@ function.def @check_type_restriction_on_param(
   %b = cast.tofelt %a : index
   function.return %b: !felt.type
 }
+// -----
+
+module attributes {llzk.lang} {
+  struct.def @C3 {
+    struct.member @f1 : !felt.type {signal}
+    function.def @compute() -> !struct.type<@C3> {
+      %self = struct.new : !struct.type<@C3>
+      function.return %self : !struct.type<@C3>
+    }
+    function.def @constrain(%self: !struct.type<@C3>) {
+      %f = struct.readm %self[@f1] : !struct.type<@C3>, !felt.type
+      // expected-error@+1 {{'cast.toindex' op only valid within a 'function.def' with 'function.allow_non_native_field_ops' attribute}}
+      %i = cast.toindex %f
+      function.return
+    }
+  }
+}

test/Dialect/Cast/type_convert_pass.llzk

@@ -1,11 +1,11 @@
 // RUN: llzk-opt -split-input-file %s 2>&1 | FileCheck --enable-var-scope %s
 
-function.def @felt_to_index(%a: !felt.type) -> index {
+function.def @felt_to_index(%a: !felt.type) -> index attributes {function.allow_non_native_field_ops} {
   %b = cast.toindex %a
   function.return %b: index
 }
 //CHECK-LABEL: function.def @felt_to_index(
-//CHECK-SAME:  %[[A0:[0-9a-zA-Z_\.]+]]: !felt.type) -> index {
+//CHECK-SAME:  %[[A0:[0-9a-zA-Z_\.]+]]: !felt.type) -> index attributes {function.allow_non_native_field_ops} {
 //CHECK-NEXT:    %[[T0:[0-9a-zA-Z_\.]+]] = cast.toindex %[[A0]]
 //CHECK-NEXT:    function.return %[[T0]] : index
 //CHECK-NEXT:  }
@@ -44,3 +44,32 @@ function.def @lt_felt(%a: !felt.type, %b: !felt.type) -> !felt.type {
 //CHECK-NEXT:    %[[T1:[0-9a-zA-Z_\.]+]] = cast.tofelt %[[T0]] : i1
 //CHECK-NEXT:    function.return %[[T1]] : !felt.type
 //CHECK-NEXT:  }
+// -----
+
+module attributes {llzk.lang} {
+  struct.def @C3 {
+    struct.member @f1 : !felt.type {signal}
+    function.def @compute() -> !struct.type<@C3> {
+      %self = struct.new : !struct.type<@C3>
+      function.return %self : !struct.type<@C3>
+    }
+    function.def @constrain(%self: !struct.type<@C3>) attributes {function.allow_non_native_field_ops} {
+      %f = struct.readm %self[@f1] : !struct.type<@C3>, !felt.type
+      %i = cast.toindex %f
+      function.return
+    }
+  }
+}
+//CHECK-LABEL: struct.def @C3 {
+//CHECK-NEXT:    struct.member @f1 : !felt.type {signal}
+//CHECK-NEXT:    function.def @compute() -> !struct.type<@C3> attributes {function.allow_witness} {
+//CHECK-NEXT:      %[[SELF:[0-9a-zA-Z_\.]+]] = struct.new : <@C3>
+//CHECK-NEXT:      function.return %[[SELF]] : !struct.type<@C3>
+//CHECK-NEXT:    }
+//CHECK-NEXT:    function.def @constrain(
+//CHECK-SAME:    %[[A0:[0-9a-zA-Z_\.]+]]: !struct.type<@C3>) attributes {function.allow_constraint, function.allow_non_native_field_ops} {
+//CHECK-NEXT:      %[[T0:[0-9a-zA-Z_\.]+]] = struct.readm %[[A0]][@f1] : <@C3>, !felt.type
+//CHECK-NEXT:      %[[T1:[0-9a-zA-Z_\.]+]] = cast.toindex %[[T0]]
+//CHECK-NEXT:      function.return
+//CHECK-NEXT:    }
+//CHECK-NEXT:  }

test/Dialect/Constrain/emit_fail.llzk

@@ -198,7 +198,7 @@ module attributes {llzk.lang} {
           %a: !struct.type<@TestComponent11>,
           %b: !struct.type<@TestComponent11>
           ) {
-      // expected-error@+1 {{'constrain.eq' op operand #0 must be any LLZK type, excluding non-Signal struct and string types, but got '!struct.type<@TestComponent11>'}}
+      // expected-error@+1 {{'constrain.eq' op operand #0 must be any LLZK type, excluding struct and string types, but got '!struct.type<@TestComponent11>'}}
       constrain.eq %a, %b : !struct.type<@TestComponent11>
       function.return
     }
@@ -217,7 +217,7 @@ module attributes {llzk.lang} {
           %a: !array.type<3 x !struct.type<@TestComponent12>>,
           %b: !array.type<3 x !struct.type<@TestComponent12>>
           ) {
-      // expected-error@+1 {{'constrain.eq' op operand #0 must be any LLZK type, excluding non-Signal struct and string types, but got '!array.type<3 x !struct.type<@TestComponent12>>'}}
+      // expected-error@+1 {{'constrain.eq' op operand #0 must be any LLZK type, excluding struct and string types, but got '!array.type<3 x !struct.type<@TestComponent12>>'}}
       constrain.eq %a, %b : !array.type<3 x !struct.type<@TestComponent12>>
       function.return
     }
@@ -236,7 +236,7 @@ module attributes {llzk.lang} {
           %a: !array.type<3,2 x !struct.type<@TestComponent13>>,
           %b: !array.type<3,2 x !struct.type<@TestComponent13>>
           ) {
-      // expected-error@+1 {{'constrain.eq' op operand #0 must be any LLZK type, excluding non-Signal struct and string types, but got '!array.type<3,2 x !struct.type<@TestComponent13>>'}}
+      // expected-error@+1 {{'constrain.eq' op operand #0 must be any LLZK type, excluding struct and string types, but got '!array.type<3,2 x !struct.type<@TestComponent13>>'}}
       constrain.eq %a, %b : !array.type<3,2 x !struct.type<@TestComponent13>>
       function.return
     }
@@ -453,7 +453,7 @@ module attributes {llzk.lang} {
       function.return %self : !struct.type<@Component24>
     }
     function.def @constrain(%a: !string.type, %b: !string.type) {
-      // expected-error@+1 {{'constrain.eq' op operand #0 must be any LLZK type, excluding non-Signal struct and string types, but got '!string.type'}}
+      // expected-error@+1 {{'constrain.eq' op operand #0 must be any LLZK type, excluding struct and string types, but got '!string.type'}}
       constrain.eq %a, %b : !string.type
       function.return
     }
@@ -469,7 +469,7 @@ module attributes {llzk.lang} {
       function.return %self : !struct.type<@Component25>
     }
     function.def @constrain(%self: !struct.type<@Component25>, %a: !array.type<2 x !string.type>, %b: !array.type<2 x !string.type>) {
-      // expected-error@+1 {{'constrain.eq' op operand #0 must be any LLZK type, excluding non-Signal struct and string types, but got '!array.type<2 x !string.type>'}}
+      // expected-error@+1 {{'constrain.eq' op operand #0 must be any LLZK type, excluding struct and string types, but got '!array.type<2 x !string.type>'}}
       constrain.eq %a, %b : !array.type<2 x !string.type>
       function.return
     }
@@ -482,7 +482,7 @@ module attributes {llzk.lang} {
 module attributes {llzk.lang} {
   struct.def @Component26 {
     function.def @constrain(%self: !struct.type<@Component26>, %b: !array.type<89 x !struct.type<@Component26>>) {
-      // expected-error@+1 {{'constrain.in' op element type must be any LLZK type, excluding non-Signal struct and string types, but got '!struct.type<@Component26>'}}
+      // expected-error@+1 {{'constrain.in' op element type must be any LLZK type, excluding struct and string types, but got '!struct.type<@Component26>'}}
       constrain.in %b, %self : !array.type<89 x !struct.type<@Component26>>, !struct.type<@Component26>
       function.return
     }

test/Dialect/POD/pod_type_fail.llzk

@@ -70,7 +70,7 @@ module attributes { llzk.lang} {
         %0: !pod.type<[@n: !string.type]>,
         %1: !pod.type<[@n: !string.type]>
     )  {
-      // expected-error@+1 {{'constrain.eq' op operand #0 must be any LLZK type, excluding non-Signal struct and string types, but got '!pod.type<[@n: !string.type]>'}}
+      // expected-error@+1 {{'constrain.eq' op operand #0 must be any LLZK type, excluding struct and string types, but got '!pod.type<[@n: !string.type]>'}}
       constrain.eq %0, %1 : !pod.type<[@n: !string.type]>
       function.return
     }