feat: add transfer-to-pbv CLI tool for PBV soundness queries

[bollu]

Summary

• Adds a new CLI tool transfer-to-pbv that reads a transfer function in the transfer. MLIR dialect (KnownBits abstract domain) and emits a PBV-format (Parametric BitVec) SMT-LIB soundness query
• Symbolically interprets the transfer function, inlining each SSA value as a PBV expression, then assembles the KnownBits soundness formula with symbolic width k
• Adds the transfer-to-pbv entry point to pyproject.toml

Details

The generated query checks: for all concrete inputs in the concretization of the abstract inputs, the concrete operation result is in the concretization of the abstract result.

KnownBits concretization: γ(k0, k1) ∋ x iff (x & k0 = 0) ∧ (x & k1 = k1), well-formedness: k0 & k1 = 0.

Supported ops: all transfer. binary/unary bitvec ops, transfer.cmp, transfer.select, transfer.constant, transfer.get_all_ones, transfer.get_bit_width, transfer.smin/smax/umin/umax, and arith.andi/ori/xori on i1.

Unsupported: count/popcount ops raise NotImplementedError (no parametric bitvector equivalent).

Usage:

transfer-to-pbv kb_Xor.mlir --concrete-op bvxor
cat kb_And.mlir | transfer-to-pbv --concrete-op bvand

Test plan

• transfer-to-pbv kb_Xor.mlir --concrete-op bvxor produces correct PBV formula
• transfer-to-pbv kb_And.mlir --concrete-op bvand produces correct PBV formula
• transfer-to-pbv kb_Add.mlir --concrete-op bvadd handles complex ops (constants, shifts)
• transfer-to-pbv kb_Shl.mlir --concrete-op bvshl handles arith boolean ops
• Unsupported ops (countl_zero etc.) raise a clear NotImplementedError

🤖 Generated with Claude Code

[bollu]

@math-fehr I'm not sure how to test this, to be honest.