Combining tensors at mismatched CKKS multiplicative levels emits arith.mulf on an integer tensor
- Dominant language
- MLIR
- Stars
- 906
- Forks
- 171
- Avg merge
- 4d 12h
- Merged PRs (30d)
- 32
Description
I've been fuzzing heir-py's `Secret[Tensor[...]]` support and found a case where the compiler generates IR that fails its own type verifier.
Combining two `Secret[Tensor[(4,), I32]]` values with `+` or `-` when they were produced by a different number of chained multiplications crashes during the CKKS lowering pipeline:
```python
from heir import compile
from heir.backends.cleartext import CleartextBackend
from heir.mlir.types import I32, Secret, Tensor
def f(x0: Secret[Tensor[(4,), I32]]) -> Tensor[(4,), I32]:
return (x0 * x0) - ((x0 * x0) * (x0 * x0))
compile(scheme="ckks", backend=CleartextBackend())(f)
```
```
error: 'arith.mulf' op operand #0 must be floating-point-like, but got 'tensor<1x1024xi32>'
note: see current operation: %8 = "arith.mulf"(%4, %1)
{mgmt.mgmt = #mgmt.mgmt}
: (tensor<1x1024xi32>, tensor<1x1024xi32>) -> tensor<1x1024xi32>
```
`arith.mulf` is the floating point multiply op, applied here to an i32 tensor. The compiler emits IR that fails its own type invariants.
`x0 * x0` costs one CKKS multiplicative level, and `(x0 * x0) * (x0 * x0)` costs two. It's specifically the mismatch that triggers this, not the values or operators involved. I checked a few contrasts to narrow it down:
- `(x0*x0) - (x1*x1)`, both 1 level, compiles fine
- `(x0*x0)*(x0*x0)` on its own compiles fine
- `((x0*x0)*(x0*x0)) - ((x1*x1)*(x1*x1))`, both 2 levels, compiles fine
- `(x1*x1) - ((x0*x0)*(x0*x0))`, 1 vs 2 levels, crashes
- Same thing with `+` instead of `-`, also crashes
- A 2 variable minimal version, `(x1*x1) - ((x1*x1)*(x1*x1))`, also crashes
So it looks like whenever two operands at different multiplicative levels get combined with a same level op like add or subtract, something needs to rescale the lower level one up to match, and that rescale step assumes the underlying type is float. CKKS scales are always real valued by construction, so for `F64` tensors this would be a no-op type match, but for an integer tensor being carried through CKKS's approximate representation, it produces this exact mismatch.
I also tried the same trigger under BGV instead of CKKS, since BGV is an exact integer scheme and I wanted to rule out this being specific to how CKKS handles integers. It doesn't reproduce the same way, but it isn't clean either, matched levels and the 2 level side alone both compile fine under BGV, and only the mismatched combination fails, this time with "Noise validation failed" instead of a type error. That looks like the same underlying level mismatch causing two different downstream symptoms depending on scheme, rather than something specific to CKKS.
Environment: heir-py 2026.8.1 from PyPI, Python 3.12, numba 0.63.0.
Happy to share the full repro script or dig further into this if it's useful.
Contributor guide
Research direction
Start by running the provided heir.compile CKKS reproducer with CleartextBackend and trace the CKKS lowering pipeline where the two tensor operands are combined at different multiplicative levels. Inspect the level-matching or rescale path and its handling of Secret[Tensor[..., I32]] values. Done means the mismatched-level + and - cases no longer emit invalid arith.mulf operations or fail verification.
Written by the indexing model from the issue text.
Assessment
- Tech stack
- python
- Domain
- compilers, cryptography
- Issue type
- Bug
- Difficulty
- 4/5
- Estimated time
- 3-5 days
- Activity status
- Active
- Clarity
- Mostly clear
- Newbie friendliness
- 48/100