Halmos fails with `Z3Exception: b'parser error'` in MODEXP

[aviggiano]

Describe the bug

When running Halmos on a relatively simple project that uses assembly, it fails wit the following error: Z3Exception: b'parser error'

To Reproduce

git clone https://github.com/aviggiano/halmos-modexp
cd halmos-modexp
halmos

Environment:

• OS: macOS
• Python version: Python 3.12.6
• Halmos and other dependency versions: halmos 0.2.1.dev16+g1502e46

Additional context

N/A

[0xkarmacoma]

thanks for the easy repro, it's an internal error. We pass an internal ByteVec type to the Z3 API, which it doesn't know how to handle. We need to unwrap it into a type that Z3 supports and add a unit test for modexp

[0xkarmacoma]

so I started working on the internal error, but if I understand your test correctly we won't be able to support it in full. The reason is that there is no modexp operator in SMT, so we can't directly ask the solver to show that it is equivalent to an actual computation.

IOW, we will support a black-box version of modexp (an "uninterpreted function" in SMT jargon), so the solver will know how to compare modexp(b1, e1, m1) to modexp(b2, e2, m2), but not to actual values

[aviggiano]

Makes sense, thanks

Is that the same as you do for the other precompiles?

[0xkarmacoma]

it's on a case by case basis, but it is the same for e.g. keccak, vm.addr, or ecrecover. Anything where we don't really have a choice but keep the values opaque to the solver