feat: prove correctness of the LLVM-dialect RISC-V combines

[tobiasgrosser]

RISCVCombines/Proofs.lean covers the combines that rewrite already-selected riscv ops, as exact equalities over the total Data.RISCV.Reg type. The 63 combines that rewrite llvm ops had no data-level lemma at all — half of Combine.lean was unproven.

Lemmas

New RISCVCombines/LLVMProofs.lean: one veir_bv_decide lemma per LLVM combine, named after the rule it justifies (so the naming convention that links Proofs.lean to Combine.lean extends to it).

LLVM ops carry poison, so the obligation is a refinement rather than an equality — the rewritten value may be more defined than the original, never less:

theorem AndSextSext {x y : Int 32} :
    and (sext x 64 h32_64) (sext y 64 h32_64) ⊒ sext (and x y) 64 h32_64 := by
  veir_bv_decide

bv_decide bitblasts and so cannot handle generic widths. These are the i64 instantiation: sext/zext from i32 to i64, trunc from i64 to i32, and i1 for select conditions and icmp results.

18 unsound combines, fixed

Writing the lemmas surfaced that 18 combines were unsound. Each copied a poison-producing flag off a matched op onto a different op it creates. Dropping a flag only removes poison and is always sound; transplanting one onto an op with a different poison condition is not.

• nsw on a hoisted shl/trunc — AndShlShl, AndTruncTrunc, and the Or/Xor variants.
• nuw/exact on hoisted Or/Xor — X alone can supply the discarded bit that poisons the created op while the source is fine. (And is safe: its bits are a subset of Y's.)
• disjoint on or — a second, independent failure in OrTruncTrunc, OrShlShl, OrLshrLshr, OrAshrAshr, OrAndAnd: X and Y may overlap only in bits the hoisted op discards.
• nneg on a hoisted zext — OrZextZext, XorZextZext.
• flag transplant onto an unrelated arithmetic op — sub_add_reg_x_sub_y_add_x, sub_add_reg_x_sub_x_add_y, add_shift, add_shift_commute, sub_one_from_sub_rw.

Concrete counterexamples, verified by #eval (each prints (source, target) as (value, poison)):

combine	flag	witness
AndShlShl	nsw	X = 2^62, Y = -2^62, Z = 1 → source 2^63, target poison
AndTruncTrunc	nsw	X = 2^31, Y = -1 → source 0x80000000, target poison
OrAndAnd	disjoint	X = 1, Y = -1, Z = -2 → source -2, target poison
sub_one_from_sub_rw	nuw	A = 5, B = 3 → source 1, target poison

Combine.lean now clears the offending flag on the created op, dropping the minimum. AndTruncTrunc and AndShlShl still keep nuw, since the bits X & Y discards are a subset of Y's. Each fix carries a comment naming its reason and pointing at its lemma; each lemma records the counterexample that motivated the clear.

With the created flag cleared, the flags read off matched ops decouple from it, so each lemma is stated with those fully free and only the created op carries a literal false:

and (shl x z s0 u0) (shl y z false u1) ⊒ shl (and x y) z false u1   -- would have been
and (shl x z s0 u0) (shl y z s1 u1)    ⊒ shl (and x y) z false u1   -- as committed

Coverage

63 → 126 of the 127 registered rules. The one remaining, li_zero_to_x0, rewrites li 0 to a read of x0; its obligation is a register-file fact, not a bitvector identity.

These are still standalone data-level identities — nothing yet ties AndSextSext-the-theorem to AndSextSext-the-rule, and Combine.lean still discharges its IR-bookkeeping obligations with sorry. Same gap as the existing Proofs.lean; wiring the two together is follow-up work.

Testing

• All 63 lemmas are sorry-free and depend only on propext, Classical.choice, Quot.sound — no sorryAx, no native_decide.
• The existing 82 RISCVCombines tests use flag-free inputs; veir-opt -p=riscv-combine output is byte-identical across all 82 before and after, so the fix only affects flag-carrying IR.
• New flag_drop_poison_safety.mlir covers nine of the fixed rules and fails against the pre-fix pass (checked), including that AndShlShl turns overflowFlags = 3 into overflowFlags = 2 rather than dropping nuw too.
• Full suite green: 647 lit tests, lake test, and a warning-clean lake build Veir (touched modules also built individually).

🤖 Generated with Claude Code

[github-actions]

VeIR Benchmarks

Details

Benchmark suite	Current: 6a17214	Previous: c6cca51	Ratio
add-fold-worklist/create	2274000 ns (± 96777)	2241000 ns (± 112014)	1.01
add-fold-worklist/rewrite	3930000 ns (± 35865)	4033500 ns (± 31734)	0.97
add-fold-worklist-local/create	2345000 ns (± 93560)	2246500 ns (± 112038)	1.04
add-fold-worklist-local/rewrite	3281000 ns (± 44696)	3391500 ns (± 73095)	0.97
add-zero-worklist/create	2362000 ns (± 84494)	2254000 ns (± 55193)	1.05
add-zero-worklist/rewrite	2628500 ns (± 119883)	2631000 ns (± 55796)	1.00
add-zero-reuse-worklist/create	1841000 ns (± 63302)	1892000 ns (± 67762)	0.97
add-zero-reuse-worklist/rewrite	2215000 ns (± 79925)	2198000 ns (± 83020)	1.01
mul-two-worklist/create	2255000 ns (± 107179)	2332000 ns (± 98767)	0.97
mul-two-worklist/rewrite	5631500 ns (± 117948)	5765000 ns (± 217745)	0.98
add-fold-forwards/create	2268000 ns (± 82373)	2219000 ns (± 41445)	1.02
add-fold-forwards/rewrite	3040000 ns (± 22961)	3071000 ns (± 21107)	0.99
add-zero-forwards/create	2302000 ns (± 111431)	2272000 ns (± 90941)	1.01
add-zero-forwards/rewrite	1915500 ns (± 42199)	1989000 ns (± 21300)	0.96
add-zero-reuse-forwards/create	1863000 ns (± 72929)	1906000 ns (± 92514)	0.98
add-zero-reuse-forwards/rewrite	1506000 ns (± 16300)	1549000 ns (± 15271)	0.97
mul-two-forwards/create	2230000 ns (± 84884)	2264000 ns (± 88706)	0.98
mul-two-forwards/rewrite	3600000 ns (± 55948)	3769000 ns (± 95668)	0.96
add-zero-reuse-first/create	1844000 ns (± 112054)	1890000 ns (± 92368)	0.98
add-zero-reuse-first/rewrite	8000 ns (± 1749)	9000 ns (± 2385)	0.89
add-zero-lots-of-reuse-first/create	1825500 ns (± 60197)	1916000 ns (± 32593)	0.95
add-zero-lots-of-reuse-first/rewrite	775000 ns (± 55349)	836000 ns (± 27463)	0.93

This comment was automatically generated by workflow using github-action-benchmark.