remove remaining uses of "Signal"

changelogs/unreleased/th__cleanup_signal_comments.yaml

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

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

@@ -36,12 +36,14 @@ 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, DeclareOpInterfaceMethods<SymbolUserOpInterface>]> {
   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. In struct @constrain functions, the argument to
+    this op is not allowed to be derived from a member with the `signal` attribute.
 
     Example:
     ```llzk
@@ -53,8 +55,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

@@ -25,11 +25,11 @@ namespace llzk::cast {
 // FeltToIndexOp
 //===------------------------------------------------------------------===//
 
-LogicalResult FeltToIndexOp::verify() {
+LogicalResult FeltToIndexOp::verifySymbolUses(SymbolTableCollection &tables) {
   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.
+      succeeded(parentOr) && !parentOr->hasAllowNonNativeFieldOpsAttr()) {
+    // Traverse the def-use chain to see if this operand, which is a felt,
+    // derives from a member with the `signal` attribute.
     SmallVector<Value, 2> frontier {getValue()};
     DenseSet<Value> visited;
 
@@ -41,11 +41,24 @@ LogicalResult FeltToIndexOp::verify() {
       visited.insert(v);
 
       if (Operation *op = v.getDefiningOp()) {
+        if (MemberReadOp read = llvm::dyn_cast<MemberReadOp>(op)) {
+          auto readFrom = read.getMemberDefOp(tables);
+          if (succeeded(readFrom) && readFrom->get().getSignal()) {
+            return emitOpError()
+                .append(
+                    "input is derived from a '", MemberDefOp::getOperationName(),
+                    "' with 'signal' attribute, which is only valid within a '",
+                    FuncDefOp::getOperationName(), "' with '", AllowNonNativeFieldOpsAttr::name,
+                    "' attribute"
+                )
+                .attachNote(read.getLoc())
+                .append("signal value is read here");
+          }
+        }
         frontier.insert(frontier.end(), op->operand_begin(), op->operand_end());
       }
     }
   }
-
   return success();
 }
 

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/Dialect/Cast/type_convert_fail.llzk

@@ -91,3 +91,21 @@ 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>) {
+      // expected-note@+1 {{signal value is read here}}
+      %f = struct.readm %self[@f1] : !struct.type<@C3>, !felt.type
+      // expected-error@+1 {{'cast.toindex' op input is derived from a 'struct.member' with 'signal' attribute, which is 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

@@ -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
     }