Combine proofs #1055
Open
tobiasgrosser wants to merge 44 commits into
Open
Conversation
`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. Add `RISCVCombines/LLVMProofs.lean` with one `veir_bv_decide` lemma per LLVM combine, named after the rule it justifies. LLVM ops carry poison, so the obligation is a refinement `source ⊒ target` rather than an equality. `bv_decide` bitblasts and so needs concrete widths: these are the `i64` instantiation, using the `i32`/`i64` pair for `sext`/`zext`/`trunc` and `i1` for `select` conditions and `icmp` results. Writing the lemmas surfaced that 18 of these combines were unsound. Each copied a poison-producing flag off a matched op onto a *different* op it creates: `nsw`/`nuw`, `exact`, a `zext`'s `nneg`, or an `or`'s `disjoint`. Dropping a flag only removes poison and is always sound, but transplanting one onto an op with a different poison condition is not. For example, `AndShlShl` kept `nsw` on the created `shl`; with `X = 2^62`, `Y = -2^62`, `Z = 1` the source evaluates to `2^63` while the rewritten program is poison. Fix all 18 in `Combine.lean` by clearing 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. With the created flag cleared, the flags read off matched ops decouple from it, so every lemma is stated with those fully free and only the created op carries a literal `false`. Each fix names its reason and points at the lemma; each lemma records the counterexample. Combine coverage goes from 63 to 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. The existing 82 `RISCVCombines` tests use flag-free inputs and their pass output is byte-identical before and after, so the fix only affects flag-carrying IR. Add `flag_drop_poison_safety.mlir`, which covers nine of the fixed rules and fails against the pre-fix pass.
`LLVMProofs.lean` proves each LLVM combine's data-level obligation, but nothing tied a theorem to the rewrite of the same name: the lemmas were free-floating `Data.LLVM.Int` refinements, matched to rules by naming convention only. Close that gap for seven combines. Port them from the `PatternRewriter` shape to `LocalRewritePattern` (`RewritePattern.fromLocalRewrite` then performs the insert/replace/erase, which removes their IR-bookkeeping `sorry`s), and prove `LocalRewritePattern.PreservesSemantics` for each in the new `CombineSemantics.lean`. That statement is about the pattern function itself, so the link is now checked by the compiler rather than by convention. Six create no operations: their local pattern returns `(ctx, some (#[], #[v]))`, so `interpretOpList [] state'` is just `state'` and the proof reduces to transporting the matched operands' refinement through the data lemma. `mulo_by_2_unsigned_signed` creates an `llvm.add` and is the op-creating exemplar, additionally replaying that operation forward in the target state. select_same_val_self, select_constant_cmp_true, select_constant_cmp_false, sub_add_reg_x_add_y_sub_y, sub_add_reg_x_add_y_sub_x, trunc_of_zext, mulo_by_2_unsigned_signed New reusable infrastructure, placed per `RewriteProofs/ProofStrategy.md`'s file map: - `matchAdd_getVar?_of_EquationLemmaAt` and `Pure.llvm_add` (Layer 3, `CommonGraphLemmas.lean`), the `add` analogue of `matchNot_getVar?_of_EquationLemmaAt`, which the `sub_add_reg` combines need to recover the defining `add`'s runtime value. - `interpretOp_llvm_binaryInt_forward` (`CommonForwardInterpret.lean`), the LLVM analogue of `interpretOp_riscv_binaryReg_forward`. Every existing forward lemma is RISC-V only; a combine, unlike a lowering, emits `llvm` operations. - `matchTruncOp_interpretOp_unfold` (`CombineSemantics.lean`), the narrowing counterpart of `matchExtOp_interpretOp_unfold`. There is no `Verified.llvm_trunc` bundle, but the pattern's own type guards supply every type fact the proof needs. `bv_decide` bitblasts and so cannot discharge a width-generic goal. The seven patterns therefore carry an `.integerType` guard and a bitwidth guard (`i32`/`i64`; `i32 -> i64 -> i32` for `trunc_of_zext`) so the data lemmas apply, and six of those lemmas are generalized from `Int 64` to `(hw : w = 64 ∨ w = 32)`. The guards narrow the rewrites: they no longer fire at `i8`. `proven_combine_width_guards.mlir` pins both directions. Move `Pure.llvm_zext` and `zext_getVar?_of_EquationLemmaAt` from `LowerSlliuw.lean` to `LowerExt.lean`, next to `matchExtOp_interpretOp_unfold`, their only real dependency. `LowerSlliuw` cannot be imported alongside `LowerBexti` (duplicate generated declaration), which is why `RewriteProofs.lean` omits it; `LowerExt` is already in the build graph. The underlying conflict between those two files is untouched. All seven proofs are `sorry`-free with the axiom footprint `ProofStrategy.md` documents. As in every instruction-selection proof, the four `Return*` predicates are hypotheses, and `fromLocalRewrite` itself still contains `sorry`s, so the chain from `PreservesSemantics` to whole-pass correctness is not yet closed. Pass output is byte-identical on all 82 pre-existing combine tests.
…bines
`(icmp pred X Y) ? X : Y -> {u,s}{max,min} X Y`, eight instances of one shape.
Following `ProofStrategy.md`'s "one proof per lowering shape, not per lowering",
factor them through a single `selectToIMinMaxLocal` combinator parameterized by the
matched predicate and the emitted intrinsic, prove its `PreservesSemantics` once, and
instantiate it eight times. Each instantiation is a single term supplying the
interpreter computation fact, the monotonicity lemma and the value-refinement lemma.
The pattern is DAG-matching: the `icmp` is reached through the `select`'s condition
operand, so recovering its runtime value needs a Layer-3 graph lemma. Add
`matchIcmp_getVar?_of_EquationLemmaAt` (and `Pure.llvm_icmp` in `CommonGraphLemmas.lean`),
the `icmp` analogue of `matchAdd_getVar?_of_EquationLemmaAt`. The emitted intrinsic is
replayed with the existing `interpretOp_llvm_binaryInt_forward`, which needed no change.
Transporting operand refinement through the emitted intrinsic needs `umax`/`umin`/`smax`/
`smin` monotonicity, which the `Data.LLVM.Int` `_mono` family was missing. Add the four,
next to `select_mono`; each is one `grind`, as the rest of the family is.
Two gotchas from `ProofStrategy.md` bit here and are worth recording: `hSemDst` is not
`rfl` for a binary op (the interpreter checks the two operand bitwidths against each
other), and with the createOp bind plus three equality guards still in `hpattern`, the
structural `grind`s blow up -- the `op.getResults` equation is now established before any
peeling, while `hpattern` is still small.
As with the previous seven, the patterns carry `.integerType` and `i32`/`i64` bitwidth
guards so the `veir_bv_decide` data lemmas apply, and the eight data lemmas are
generalized from `Int 64` to `(hw : w = 64 ∨ w = 32)`. The rewrites no longer fire at
`i8`; `proven_combine_width_guards.mlir` pins that.
Graph-level coverage: 7 -> 15 of the 127 registered combines. All fifteen are sorry-free
with the axiom footprint `ProofStrategy.md` documents. `Combine.lean` drops from 254 to
230 sorry-lines. The registered pattern list is unchanged and pass output is
byte-identical on all 82 pre-existing combine tests.
`(x & y) ^ y -> (~x) & y`. Port `xor_of_and_with_same_reg` from the `PatternRewriter`
shape to `LocalRewritePattern` form (dropping its IR-bookkeeping `sorry`s and adding the
`.integerType` + `i32`/`i64` width guard), and prove its graph-level
`LocalRewritePattern.PreservesSemantics` in `CombineSemantics.lean`.
`op` is the `xor`, whose first operand is the result of a defining `and x y` sharing the
second operand `y`; recover the `and`'s value with the generic
`matchBinop_getVar?_of_EquationLemmaAt`, then create three ops -- `constant -1`,
`xor x (-1)` (`~x`), and `and (~x) y` -- replayed forward in the target state. The
assembly transports the refined `x`/`y` through `xor_mono`/`and_mono`.
New reusable piece: `OperationPtr.Pure.llvm_and` in `CommonGraphLemmas.lean`. The
data lemma `xor_of_and_with_same_reg` in `LLVMProofs.lean` is generalized from `i64` to
`w in {64, 32}`.
Full `Veir` builds clean; `#print axioms` is the accepted baseline (no `sorry`).
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
`(A - B) - 1 -> (~B) + A`. Port `sub_one_from_sub_rw` to `LocalRewritePattern` form
(dropping its IR-bookkeeping `sorry`s, adding the `.integerType` + `i32`/`i64` width
guard) and prove `LocalRewritePattern.PreservesSemantics` in `CombineSemantics.lean`.
`op` is the outer `sub`, whose second operand is the constant `1` (pinned via
`matchConstantIntVal_getVar?_of_EquationLemmaAt`) and whose first operand is the result
of a defining `sub A B` (recovered via the generic `matchBinop_getVar?`). It creates a
`constant -1`, an `xor B (-1)` (`~B`), and an `add (~B) A` with cleared flags, replayed
forward; the refined `A`/`B` are transported through `xor_mono`/`add_mono`. The created
`add` clears `nsw`/`nuw` (the matched subs' flags stay free), matching the counterexample
in the data lemma's docstring.
The data lemma `sub_one_from_sub_rw` in `LLVMProofs.lean` is generalized from `i64` to
`w in {64, 32}`.
Full `Veir` builds clean; `#print axioms` is the accepted baseline (no `sorry`).
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
`select c 0 1 -> zext (~c)` and `select c 0 -1 -> sext (~c)`, the swapped-arm cousins of
`select_1_0`/`select_neg1_0`. Factor them through one `matchSelectNotExtLocal` combinator
(match `select c 0 C1` with `C1 in {1, -1}`, emit `constant -1` + `xor c (-1)` (`~c`) +
`{zext,sext} (~c)`), port to `LocalRewritePattern` form dropping the IR-bookkeeping
`sorry`s and adding the `.integerType` + `i32`/`i64` result-width guard, and prove the
shared `LocalRewritePattern.PreservesSemantics` once, instantiated twice.
The proof peels `matchSelect`, the result-type/width guards and both constant arms
(pinned via `matchConstantIntVal_getVar?_of_EquationLemmaAt`), creates the three ops on
`i1` (`constant`, `xor`) then the width-changing extension (replayed with
`interpretOp_llvm_unaryInt_forward`), and transports the refined `c` through
`xor_mono` and the extension's monotonicity. Reuses `zext_interpretOp'`/`sext_interpretOp'`
and `zext_mono`/`sext_mono`.
The data lemmas `select_0_1`/`select_0_neg1` in `LLVMProofs.lean` are generalized from
`i64` to `w in {64, 32}`.
Full `Veir` builds clean; `#print axioms` is the accepted baseline (no `sorry`).
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
`(X & Z) op (Y & Z) -> (X op Y) & Z` for `op in {and, or, xor}` (the `*AndAnd` subfamily
of `hoist_logic_op_with_same_opcode_hands`). Factor all three through one `hoistAndAndLocal`
combinator (both operands of the outer op recovered through defining `and _ Z` sharing `Z`,
emitting `inner = dst X Y` then `and inner Z`), port to `LocalRewritePattern` form (dropping
the IR-bookkeeping `sorry`s, adding the `.integerType` + `i32`/`i64` guard), and prove the
shared `LocalRewritePattern.PreservesSemantics` once, instantiated three times.
The proof is the two-branch-DAG-matching shape (like `double_icmp_zero`) with no width
mixing: recover both defining `and`s via the generic `matchBinop_getVar?_of_EquationLemmaAt`,
create the inner `dst X Y` and outer `and inner Z`, replay both forward, and transport the
refined `X`/`Y`/`Z` through the inner op's monotonicity and `and_mono`. `OrAndAnd`'s created
`or` clears `disjoint` (the outer `or`'s flag is dropped), matching the data lemma.
`matchBinopNoProps` is moved earlier in `Combine.lean` so `hoistAndAndLocal`'s instances can
reference it. The data lemmas `AndAndAnd`/`OrAndAnd`/`XorAndAnd` in `LLVMProofs.lean` are
generalized from `i64` to `w in {64, 32}`.
Full `Veir` builds clean; `#print axioms` is the accepted baseline (no `sorry`).
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…extZext
`(zext X) op (zext Y) -> zext (X op Y)` for `op in {and, or, xor}`, at `i32 -> i64` (the
`*ZextZext` subfamily of `hoist_logic_op_with_same_opcode_hands`). Factor all three through
one `hoistZextLocal` combinator (both operands recovered as defining `zext`s via
`zext_getVar?_of_EquationLemmaAt`, emit `inner = dst X Y` at `i32` then `zext inner` at
`i64`), port to `LocalRewritePattern` form dropping the IR-bookkeeping `sorry`s and adding
the narrow-`{32}`/result-`{64}` width guards, and prove the shared
`LocalRewritePattern.PreservesSemantics` once, instantiated three times.
The created `zext` threads `nneg` dynamically: `AndZextZext` reuses the second `zext`'s
`nneg` (`useSndNneg := true`); `OrZextZext`/`XorZextZext` clear it, and the created `or`
additionally clears `disjoint` (both are sound because a never-poison target only increases
definedness). Replay uses `interpretOp_llvm_binaryInt_forward` for the narrow op and
`zext_interpretOp'` for the widening, transporting the refined `X`/`Y` through the inner op's
monotonicity and `zext_mono`.
The data lemmas `AndZextZext`/`OrZextZext`/`XorZextZext` in `LLVMProofs.lean` keep `i32->i64`;
`OrZextZext`'s created `or` is set to `disjoint := false` to match the emitted op.
Full `Veir` builds clean; `#print axioms` is the accepted baseline (no `sorry`).
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…extSext
`(sext X) op (sext Y) -> sext (X op Y)` for `op in {and, or, xor}`, at `i32 -> i64` (the
`*SextSext` subfamily of `hoist_logic_op_with_same_opcode_hands`). Factor all three through
one `hoistSextLocal` combinator, mirroring `hoistZextLocal` but simpler (`sext` carries no
`nneg`): both operands recovered as defining `sext`s, emit `inner = dst X Y` at `i32` then
`sext inner` at `i64`. Port to `LocalRewritePattern` form (dropping the IR-bookkeeping
`sorry`s, adding the narrow-`{32}`/result-`{64}` width guards) and prove the shared
`LocalRewritePattern.PreservesSemantics` once, instantiated three times.
New reusable pieces in `LowerExt.lean`: `OperationPtr.Pure.llvm_sext` and
`sext_getVar?_of_EquationLemmaAt` (the `sext` analogue of `zext_getVar?_of_EquationLemmaAt`,
built on `matchExtOp_interpretOp_unfold` / `sext_interpretOp'`). `OrSextSext`'s created `or`
clears `disjoint` to match the emitted op; the data lemma is updated accordingly.
Full `Veir` builds clean; `#print axioms` is the accepted baseline (no `sorry`).
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Add graph-level LocalRewritePattern.PreservesSemantics proof for the
select_of_zext combine (zext (select c t f) -> select c (zext t) (zext f)).
- Add interpretOp_llvm_select_forward to CommonForwardInterpret for
replaying an emitted llvm.select (i1 cond + two i{w} arms).
- Complete select_of_zext_local_preservesSemantics: peel the defining
select, recover c/t/f, replay the two zexts and the new select, and
assemble via select_of_zext_rw + select_mono + zext_mono.
Full Veir builds; #print axioms shows baseline axioms only, no sorry.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Port `AndTruncTrunc`/`OrTruncTrunc`/`XorTruncTrunc` from raw `PatternRewriter`
defs (12 `sorry`s) to a `hoistTruncLocal` `LocalRewritePattern` combinator, and
prove it correct once, generically over the outer op:
(trunc X) outer (trunc Y) -> trunc (X outer Y) outer in {and, or, xor}
The narrowing mirror of `hoistZextLocal`. Adds the `i64 -> i32` width guards the
data lemmas need (the combines were previously width-generic, while
`Data.LLVM.Int.{And,Or,Xor}TruncTrunc` only hold at that width pair).
- Verifier: `IsVerifiedTruncop` + `Verified.llvm_trunc`. Stated conditionally on
the result being an integer type, since `verifyTruncTypes` also admits byte
operands; a caller who knows the result is an integer recovers exactly the
`IsVerifiedIntegerExtop` facts and the byte arm never arises.
- CombineSemantics: `trunc_interpretOp'`, `Pure.llvm_trunc`, and the Layer-3
graph lemma `trunc_getVar?_of_EquationLemmaAt` (narrowing analogue of
`zext_getVar?_of_EquationLemmaAt`).
- `hoistTruncLocal_preservesSemantics` + the three instantiations.
Zero `sorry`; `Combine.lean` drops from 217 to 205.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…shrAshr Replace the three sorry-ridden raw PatternRewriter defs with a single hoistAshrLocal combinator (LocalRewritePattern form) plus three RewritePattern.fromLocalRewrite instances, and prove the shared hoistAshrLocal_preservesSemantics combinator theorem with the three instantiations. Adds OperationPtr.Pure.llvm_ashr locally in CombineSemantics.lean. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…tchas - Layer 1: when an opcode's verifier accepts more than the integer shape (`llvm.trunc` also admits byte operands), state the `IsVerified*` bundle conditionally on the result being an integer rather than as a disjunction. - Gotchas: `grind` can emit an `Attribute.noConfusion` term the kernel rejects on vacuous branches (use `exfalso; simp_all; done`), and `by grind` cannot build a `TypeAttr` subtype element from a bare `.val` equation. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Replace the three sorry-filled PatternRewriter defs (AndLshrLshr,
OrLshrLshr, XorLshrLshr) with a single LocalRewritePattern combinator
hoistLshrLocal, mirroring hoistAndAndLocal/hoistZextLocal, and prove its
correctness via hoistLshrLocal_preservesSemantics.
Because llvm.lshr verifies as IsVerifiedLLVMShift (not
IsVerifiedIntegerBinop), the defining shifts' runtime values are
recovered via a new graph lemma matchLshr_getVar?_of_EquationLemmaAt,
the arbitrary-shift-amount generalization of
lshrConst_getVar?_of_EquationLemmaAt, recovering the operand-width
equality dynamically through matchShiftOp_interpretOp_unfold.
Data obligations reuse Data.LLVM.Int.{And,Or,Xor}LshrLshr and the
{and,or,xor,lshr}_mono lemmas.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Silences the `linter.unusedSimpArgs` warning in `hoistLshrLocal_preservesSemantics`: after both bitwidths are substituted to literals, the `IntegerType.bitwidth` unfold at `hwV` is a no-op. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Replace the three sorry-laden `PatternRewriter` defs with a single
`hoistShlLocal` `LocalRewritePattern` combinator (mirroring
`hoistZextLocal`): both operands defined by `llvm.shl` with the same shift
amount, i64 width guards, emitting `(X outer Y) << Z`.
`CombineSemantics.lean` adds `OperationPtr.Pure.llvm_shl`, a shift-flavoured
graph lemma `matchShl_getVar?_of_EquationLemmaAt` (recovers the operand-width
equality dynamically from the successful source interpretation via
`matchShiftOp_interpretOp_unfold`, since `llvm.shl` verifies only as
`IsVerifiedLLVMShift`), the shared proof `hoistShlLocal_preservesSemantics`,
and the three instantiations `AndShlShl_local_preservesSemantics` /
`OrShlShl_local_preservesSemantics` / `XorShlShl_local_preservesSemantics`.
Data obligations reuse `Data.LLVM.Int.{AndShlShl,OrShlShl,XorShlShl}` and the
existing `shl_mono` / `{and,or,xor}_mono`.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Convert the two `add_shift` raw PatternRewriter defs into a single `addShiftLocal (commuted : Bool)` LocalRewritePattern combinator (width guards pinning the shift amount and result to i64) and prove semantics preservation of both instances. The pattern is a three-level DAG match: op is `add`; one operand is a defining `shl`; that `shl`'s first operand is a defining `sub`; that `sub`'s first operand is a defining `constant 0`. A new private core lemma `shlNegChain` walks the `shl -> sub -> constant` chain (building the strictlyDominates chain by hand with `strictlyDominates_trans`), then `addShiftLocal_preservesSemantics` unfolds the `add`, re-emits `sub A (shl B C)`, and closes with the existing data lemmas `Data.LLVM.Int.add_shift` / `add_shift_commute` plus sub/shl monotonicity. Adds `OperationPtr.Pure.llvm_shl` to CommonGraphLemmas.lean. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
The `hoistShlLocal` and `addShiftLocal` proofs were developed in parallel and each introduced an `OperationPtr.Pure.llvm_shl`. They landed in different namespaces (`Veir.RISCV.` vs `Veir.`) so the build was green, but keeping both is a trap. Keep the one in `CommonGraphLemmas.lean`, beside the other purity facts, and drop the copy in `CombineSemantics.lean`. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…nst combines Replace the five sorry-laden `commute_const_*` PatternRewriter defs with a single `commuteConstLocal` combinator (LocalRewritePattern form) and prove `commuteConstLocal_preservesSemantics` once, generic over the binop opcode, then instantiate for add/mul/and/or/xor. The rewrite `OP (const C) X -> OP X (const C)` is width-generic: commutativity holds at every bitwidth, and every flag (nsw/nuw/disjoint) is symmetric under commutation so `props` passes through unchanged. Add flag-carrying commutativity lemmas `add_comm_flags`/`and_comm`/`or_comm`/`xor_comm` to Data/LLVM/Int/Lemmas.lean (mul_comm already existed). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Port shl/lshr/ashr/mul_left_to_zero (0 op X -> 0) to LocalRewritePattern form via a shared `binopZeroLeftLocal` combinator, and prove `PreservesSemantics` for all four. Width-generic (no bitwidth guard): the data lemmas discharge directly from `isRefinedBy_iff` since `0 op X` is either 0 or (for shifts, X >= bitwidth) poison, and `poison ⊒ 0`. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Rewrite the three trunc(binop X C) -> binop(trunc X)(trunc C) combines in LocalRewritePattern form via a shared `narrowBinopLocal` combinator, and prove `narrowBinopLocal_preservesSemantics` plus the three instantiations. Flag-soundness fix: the previous defs transplanted the outer trunc's nsw/nuw onto BOTH created operand truncs. That is unsound (truncating X or C alone has a different poison condition than truncating X binop C), so the combinator now clears nsw/nuw on the operand truncs as well as the narrowed binop. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Rewrite the three cast-chain combines as LocalRewritePatterns and prove PreservesSemantics for each. zext_of_zext/sext_of_sext share the new castOfCastLocal combinator (cast (cast x) -> cast x, i8->i32->i64); truncate_of_sext (trunc (sext x) -> x) mirrors trunc_of_zext. The created zext drops the outer nneg: the outer zext inspects the inner zext's always-non-negative result, so keeping nneg would transplant poison onto `zext x` whose operand x can be negative. Data lemmas trunc_of_sext / zext_of_zext / sext_of_sext added to LLVMProofs; proofs in CombineSemantics. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
`APlusC1MinusC2`, `C2MinusAPlusC1`, `AMinusC1MinusC2`, `C1MinusAMinusC2`, `AMinusC1PlusC2` are ported to `LocalRewritePattern` form and proven. SOUNDNESS FIX: the previous defs transplanted the matched op's `nsw`/`nuw` onto the created arithmetic op. That is unsound — folding the two constants changes the overflow condition, so the created op could be poison where the source is defined (`nuw`, `A=5, C1=0, C2=3`: source `(5+0)-3 = 2` is defined, target `add nuw 5 (0-3)` wraps). All five now clear `nsw`/`nuw` on the created op. The combines also gain `i32`/`i64` bitwidth guards, which they previously lacked entirely, so they no longer fire at widths where nothing is proven. Adds the `Int`->`BitVec` bridge `ofInt_add_norm`/`ofInt_sub_norm` (Bitblast), the graph lemma `matchBinopFstConst_getVar?_of_EquationLemmaAt`, and the five `veir_bv_decide` data lemmas. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Port the four combines to a shared `subNegMinMaxLocal` combinator and prove it.
SOUNDNESS FIX: the previous defs created the inner `sub 0 a` carrying the OUTER
matched `sub`'s `nsw`/`nuw`. Those flags constrain `0 - minmax(..)`, whose
overflow condition differs from `0 - a`'s, so transplanting them could poison
the created op where the source is defined. The inner sub is now created with
`{nsw := false, nuw := false}`; clearing a flag only removes poison and is
unconditionally sound for `source ⊒ target`. The four data lemmas leave every
matched flag free, confirming the rewrite holds for all flag combinations.
Adds `Pure.llvm_intr__{smax,smin,umax,umin}` (CommonGraphLemmas) and the four
`veir_bv_decide` data lemmas.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
The combine `lshr (trunc (lshr x, C1)), C2 → trunc (lshr x, (C1 + C2))` was UNSOUND as written. For x = 2^37, C1 = 5, C2 = 3 (the exact constants the test used) the source computes `lshr (trunc (lshr x 5)) 3 = lshr (trunc 2^32) 3 = 0` while the target computes `trunc (lshr x 8) = trunc 2^29 = 2^29` — two distinct concrete values, so `source ⊒ target` fails. The transform is only valid when the truncation drops no live bit of `x >>u C1` (w1 - C1 ≤ w2, here 32 ≤ C1) AND the fused shift stays in range (C1 + C2 < w1). The old def also transplanted the matched shifts' `exact` flags onto the created `lshr` at the fused amount C1+C2, whose poison condition differs. Rewrites the combine as a sound `lshr_of_trunc_of_lshr_local` (LocalRewrite style, `createOp!` — no `sorry`) with the guard `32 ≤ C1 ∧ 0 ≤ C2 ∧ C1 + C2 < 64`, at the test widths x : i64 / result : i32, and drops the created `lshr`/`trunc` flags. Updates the lit test to C1 = 40, C2 = 3 (both guards hold; folds to lshr by 43). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Rewrite the two funnel-shift-by-zero combines as LocalRewritePatterns via a shared combinator funnelShiftZeroLocal (fshl x y 0 -> x, fshr x y 0 -> y), removing their sorry-based replaceValue/eraseOp bodies. Prove the shared combinator correct (funnelShiftZeroLocal_preservesSemantics) and instantiate for both. Width-generic data lemmas fshl_zero_amt/fshr_zero_amt in LLVMProofs. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
`sub a (mul x C)` -> `add a (mul x (-C))` for a constant `C`.
SOUNDNESS FIX: the previous def transplanted the matched `mul`'s `nsw`/`nuw`
onto the created `mul x (-C)`. Negating the constant changes the overflow
condition, so a defined source can become a poison target: at i8, `x = -128,
C = 1` gives `mul nsw x C = -128` (fits) but `mul nsw x (-C) = 128` (overflows).
The created `mul` now carries `{nsw := false, nuw := false}`; clearing a flag
only removes poison and is sound for `source ⊒ target`. The matched ops' flags
stay free variables in the proof, so the rewrite is proven for every setting.
The data lemma `SubMulConst` is width-generic — `a - x*C = a + x*(-C)` is a ring
identity, proved by rewriting through `BitVec.mul_neg` rather than `bv_decide`,
so no bitwidth guard is needed. Adds the `ofInt_neg_norm` bridge to Bitblast.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Refactor `select_not` and `canonicalize_icmp` from raw `sorry`-carrying `PatternRewriter` defs into `LocalRewritePattern` form (`selectNotLocal`, `canonicalizeIcmpLocal` + `fromLocalRewrite` wrappers) and prove their `PreservesSemantics`. - `select_not`: `select (not c) x y -> select c y x`. Two-level DAG match (condition is a defining `xor c -1`, via `matchNot_getVar?_of_EquationLemmaAt`), emits one swapped `llvm.select`. Guarded to integer arms (width-generic). - `canonicalize_icmp`: `icmp pred C x -> icmp (swapped pred) x C`. Width-generic. Data lemmas `select_not_swap` and `icmp_swap` (both equalities) added to LLVMProofs.lean; new theorems `selectNotLocal_preservesSemantics` and `canonicalizeIcmpLocal_preservesSemantics` appended to CombineSemantics.lean. No Verifier/Bitblast changes. No flag concerns (both carry only a predicate / unit properties). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Every proof in CombineSemantics.lean so far concerned `llvm.*` ops. This adds
the register-level scaffolding and uses it to prove the six idempotent-extension
folds (`{s,z}ext{b,h,w}` of the same extension) via one `drop_redundant_ext_local`
combinator.
`Data.RISCV.Reg` is total, so `RuntimeValue.reg` refinement is plain equality and
the data obligations are equalities rather than refinements.
New shared machinery, which unblocks the remaining riscv-dialect combines:
- `LocalRewritePattern.exists_refined_reg_getVar?` (CommonBaseLemmas) -- the
register-operand reader, the analogue of `exists_refined_int_getVar?`.
- `Pure.riscv_{sextb,sexth,sextw,zextb,zexth,zextw}`,
`matchRiscvUnaryReg_interpretOp_unfold`, and
`riscv_unaryReg_getVar?_of_EquationLemmaAt` (CommonGraphLemmas). The unfold
recovers operand register-ness from the *interpretation* rather than the
verifier, since the riscv verifier arms only check operand/result counts.
No verifier bundle was needed. Behaviour is unchanged: the six combines keep
their names and registration, and only move to `LocalRewritePattern` form.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
`or (and x y) x -> x` and `or x (and x y) -> x`, via one `orOfAndLocal (andOnLeft : Bool)` combinator. Pure value replacement, no ops created. The `or`'s `disjoint` flag is left a FREE VARIABLE in the data lemmas, so the combines are proven sound for every setting: when `disjoint` is set and the operands overlap the source is poison and `poison ⊒ x`; otherwise `(x & y) | x = x` by absorption. No flag transplant is possible here and none was found. The lemmas are width-generic, so no bitwidth guard is needed. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
`sub x (const C)` -> `add x (const -C)`, and the riscv-dialect `riscv.add x (riscv.li 0)` -> `x`. No soundness bug: `sub_to_add` was already clearing `nsw`/`nuw` on the created `add`, and that is necessary — `add nuw x (-C)` overflows exactly when `x >= C`, i.e. precisely when the source `sub nuw x C` is defined. `right_identity_zero_add` is the second riscv-dialect proof. Its `.riscv .add` and `.li` verifier arms only check operand/result counts and do not pin register-typedness, so register values are recovered from the interpreter's own `[.reg, .reg]` match on a successful interpretation rather than from a `Verified.riscv_add` bundle. Adds `right_identity_zero_add_comm` to Proofs.lean (the interpreter computes `RISCV.add op2 op1`, so the operand order is flipped). Drops this branch's private `exists_refined_reg_getVar?` in favour of the identical `LocalRewritePattern.exists_refined_reg_getVar?` that landed in CommonBaseLemmas.lean, and its duplicate `ofInt_neg_norm` in favour of the one already in Bitblast.lean — both were written twice by agents working in parallel. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…t,right} `or (fshl x z y) (shl x y) -> fshl x z y` and the `fshr`/`lshr` mirror. Both operand orders of the commutative `or` are handled. Value-replacement combines: no ops are created, so no flag can be transplanted; the shift flags and the `or`'s `disjoint` appear only on the source side, where extra poison is sound. Adds the ternary graph lemma `matchTernaryOp_getVar?_of_EquationLemmaAt` and `Pure.llvm_intr__fshl`/`fshr` (CommonGraphLemmas), reusing the existing `matchShl_getVar?`/`matchLshr_getVar?_of_EquationLemmaAt` for the shift level. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…mbines
Convert the `riscv.<ext> (riscv.li v) -> riscv.li v` folds to `LocalRewritePattern`
form and prove `PreservesSemantics`:
- `ext_li_range_local` (generic over ext/lo/hi), with `zextw_li_low32`,
`sextw_li_low32`, `zextb_li_low8`, `zexth_li_low16`, `sextb_li_low8`,
`sexth_li_low16` as instantiations.
- Shared proof `ext_li_range_local_preservesSemantics` plus the six
`*_local_preservesSemantics` instances; the obligation is the register
equality `f (li (ofInt 64 v)) = li (ofInt 64 v)` on `[lo, hi)`.
- `Int`-range data lemmas `{zextb,zexth,zextw,sextb,sexth,sextw}_li_ofInt`
in Proofs.lean, bridging the immediate's `Int` bound to the materialised
value's bit pattern via toNat/toInt.
All guard ranges verified against each ext's width (zero-ext `[0,2^w)`,
sign-ext `[-2^(w-1),2^(w-1))`); no soundness change.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
`riscv.li 0 -> rv64.get_register x0` is proven. Adds the forward-replay lemma `interpretOp_rv64_get_register_forward` (the first proof here to create an `rv64.get_register`) and the data equality `li_ofInt_zero_eq_x0`. `ext_x0` (`riscv.<ext> x0 -> x0`) is deliberately LEFT UNPROVEN and unchanged. It is unsound as written: it keys off the *declared* register-type index `some 0`, but nothing in the interpreter forces an `!riscv.reg<x0>`-typed value to be zero. `Conforms (.reg _) (registerType _)` is `True`, and the `unrealized_conversion_cast` arm matches `.registerType _` with a wildcard, ignoring the index. Only `rv64.get_register` reads zero. Demonstrated end to end: a module casting `2^40` into an `!riscv.reg<x0>` and applying `riscv.zextw` returns 0; after `-p=riscv-combine` deletes the `zextw`, the same module returns 2^40. To be sound, `ext_x0` must key on its operand being *defined by* `rv64.get_register x0` (the mirror of `li_zero_to_x0`), not on the declared type. Left for a follow-up since it changes matching behaviour. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
`riscv.<ext> (riscv.<dst> a b) -> riscv.<dst> a b` for dst in {and, or, xor} and
ext in {zextw, zextb, zexth, sextw, sextb, sexth}, when the guarded operands
already establish the bit pattern the outer extension would impose.
The `oneOperandSuffices` flag is confirmed correct by construction: the generic
theorem consumes the single-operand data facts only when the flag is set (the
three zero-extending `and` cases) and the both-operands fact otherwise. A wrong
flag would demand a false data lemma and the proof would not close.
Adds `matchRiscvBinaryReg_interpretOp_unfold`,
`riscv_binaryReg_getVar?_of_EquationLemmaAt`,
`riscv_unaryReg_getVar?_of_strictlyDominates`, and `Pure.riscv_{and,or,xor}`
(CommonGraphLemmas). All required `Data.RISCV.Reg` equalities already existed in
`Proofs.lean`.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…erators
Ten registered patterns:
- `drop_slli_srli_boolLocal` : `srli (slli b 63) 63 -> b` when `b` is produced by
one of slt/sltu/slti/sltiu/seqz/snez/sltz/sgtz (all eight instantiated).
- `srl_sra_signbitLocal` : `srl (sra x k) (w-1) -> srl x (w-1)`, at both
`srli`/`srai`/64 and `srliw`/`sraiw`/32.
Soundness checked against the interpreter, not the comments: the eight boolean
ops all yield `setWidth 64 (ofBool _)` in {0,1}, and the W-variants operate on
bits 31:0 so `width-1 = 31` isolates the 32-bit sign bit. No bug found here.
Adds `matchRiscvUnaryRegImm_interpretOp_unfold`,
`riscv_unaryRegImm_getVarBoth_of_EquationLemmaAt`, `riscv_result_interpretOp_unfold`,
`riscv_bool_getVar?_of_EquationLemmaAt` and eleven `Pure.riscv_*` facts
(CommonGraphLemmas), plus `drop_slli_srli_of_bit` and nine `*_bit` range lemmas
(Proofs).
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…d family
SOUNDNESS FIX (miscompile). `riscv.sw`/`sh`/`sb` take `(value, address)` — the
interpreter destructures `[.reg { val }, .reg addr]` and isel emits
`#[value, pointer]`. But `matchRiscvStore` returned `(operands[0], operands[1])`
named `(addr, val)`, inverted. So `drop_ext_store` stripped the extension off the
ADDRESS operand (unsound: the 64-bit pointer lost its high bits) and never
touched the VALUE operand (a missed optimization).
Root cause: efce87d ("fix: riscv store operand order") updated the interpreter,
isel, and the Interpreter tests, but not RISCVCombines. The three store lit tests
here were written against the stale convention, so they passed while asserting
the unsound behaviour; they are corrected, not weakened.
Reproduced before the fix with `veir-opt -p=riscv-combine`: an extension on the
address was deleted, on the value retained. After: the reverse, as intended.
Also proves 10 registered patterns:
- `drop_ext_unary_imm_low_word_local_preservesSemantics` + 8 instantiations
(`drop_{zextw,sextw}_{addiw,roriw,srliw,sextw|zextw}`)
- `drop_ext_binary_low_word_local_preservesSemantics` + `drop_{zextw,sextw}_addw`
Each `dst` re-verified against the interpreter to read only bits 31:0.
`drop_ext_store` is converted and its soundness fix landed, but PreservesSemantics
is not proven: it is the only obligation here touching the memory component, and
needs a store-interpretation unfold, a store forward lemma, and a
bytearray/extractLsb bridge. Left for a follow-up rather than forced.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Cherry-picked from upstream tobias/proofs-combines (86cd363), which is independent of that branch's *TruncTrunc commit; our `hoistTruncLocal` (useSndNuw) and `IsVerifiedTruncop` are retained per the earlier decision. Rebased by hand: git's three-way merge interleaved the two proofs, so the two upstream blocks (`matchSelect_baseType_eq_tvType` and the `select_of_truncate_local_preservesSemantics` section) were re-appended at the tail, where all their dependencies are already in scope. Also silences three lints the upstream block carried (an unreferenced `ctxDom` binder and two unused `dif_neg` simp arguments) to keep the tree warning-free. Co-Authored-By: Osman Yasar <osmanyas05@gmail.com> Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.