LLZK-to-ZKLean conversion silently drops zero-result constraint operations

[Kuhai9801]

Summary

--convert-llzk-to-zklean can silently erase constraint operations that have no SSA results.

I found two cases:

1. constrain.in is dropped from the converted function body.
2. function.call to another function.allow_constraint function is dropped from the caller body.

In both cases the pass exits successfully and emits ZKLean IR, but the emitted artifact has fewer constraints than the source LLZK program.

Reproduction

Tested against project-llzk/llzk-lib main at:

30b0fa1eb77de154ff60c13fa88ef286d8b01c65

Case 1: constrain.in is dropped

Input:

module attributes {llzk.lang = "llzk"} {
  function.def @contains(%xs: !array.type<2 x !felt.type<"babybear">>, %x: !felt.type<"babybear">) attributes {function.allow_constraint} {
    constrain.in %xs, %x : !array.type<2 x !felt.type<"babybear">>, !felt.type<"babybear">
    function.return
  }
}

Run:

llzk-opt repro-constrain-in.llzk --convert-llzk-to-zklean

Observed output:

module @ZKLean attributes {llzk.lang = "llzk"} {
  func.func @contains(%arg0: !array.type<2 x !felt.type<"babybear">>, %arg1: !felt.type<"babybear">) {
    return
  }
}

The source function contains a constrain.in, but the converted ZKLean function body contains only return.

Case 2: constraint helper call is dropped from caller

Input:

module attributes {llzk.lang = "llzk"} {
  struct.def @Child {
    struct.member @out : !felt.type<"babybear">

    function.def @compute(%x: !felt.type<"babybear">) -> !struct.type<@Child> {
      %self = struct.new : !struct.type<@Child>
      struct.writem %self[@out] = %x : !struct.type<@Child>, !felt.type<"babybear">
      function.return %self : !struct.type<@Child>
    }

    function.def @constrain(%self: !struct.type<@Child>, %x: !felt.type<"babybear">) attributes {function.allow_constraint} {
      %one = felt.const 1 <"babybear">
      constrain.eq %x, %one : !felt.type<"babybear">
      function.return
    }
  }

  function.def @parent(%child: !struct.type<@Child>, %x: !felt.type<"babybear">) attributes {function.allow_constraint} {
    function.call @Child::@constrain(%child, %x) : (!struct.type<@Child>, !felt.type<"babybear">) -> ()
    function.return
  }
}

Run:

llzk-opt repro-call.llzk --convert-llzk-to-zklean

Observed output includes a converted child constraint:

func.func @Child__constrain(%arg0: !ZKLeanLean.type<@Child>, %arg1: !felt.type<"babybear">) {
  %felt_const_1 = felt.const  1 : <"babybear">
  %0 = ZKExpr.Literal %felt_const_1
  %1 = ZKExpr.Literal %arg1
  %2 = ZKBuilder.ConstrainEq %1 %0
  return
}

But the caller body is empty:

func.func @parent(%arg0: !ZKLeanLean.type<@Child>, %arg1: !felt.type<"babybear">) {
  return
}

So @Child__constrain is emitted, but the @parent function no longer enforces the call to it.

Expected behavior

The converter should preserve constraint semantics, or fail loudly when it cannot.

For unsupported zero-result operations, I would expect something like:

• emit a diagnostic,
• set the conversion error state,
• fail --convert-llzk-to-zklean.

For supported operations, the ZKLean output should contain equivalent constraints. In particular, a function.call from one function.allow_constraint function to another should not disappear from the caller body.

Actual behavior

The pass exits successfully and emits ZKLean IR.

Unsupported zero-result operations appear to fall through without producing output and without causing conversion failure. This is different from unsupported result-producing operations, which do report an unsupported-op error.

Impact

The converted ZKLean artifact can be weaker than the LLZK source program.

This matters because the output of --convert-llzk-to-zklean may look like a successful translation, while constraints from the source have been erased. A downstream consumer of the generated ZKLean IR would see a different constraint system from the one expressed in LLZK.

Likely fix area

The issue appears to be in the per-operation conversion logic here:

backends/zklean/lib/Conversions/LLZKToZKLean.cpp

The current conversion handles known operations such as felt.const, arithmetic ops, struct.readm, and constrain.eq. At the end, unsupported operations are only rejected when op->getNumResults() != 0.

That leaves unsupported zero-result operations, including constrain.in and function.call, able to fall through silently.

A minimal fix would be to explicitly reject unhandled zero-result operations, excluding only operations that are intentionally no-ops such as function.return. A fuller fix could lower constrain.in and constraint-function calls where those are intended to be supported.