feat(interpret): prove interpretOp' monotone - #774
Draft
tobiasgrosser wants to merge 9 commits into
Draft
Conversation
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?s=60&v=4){kind=small}
Contributor
There was a problem hiding this comment.
VeIR Benchmarks
Details
| Benchmark suite | Current: dd42387 | Previous: 9f42ace | Ratio |
|---|---|---|---|
add-fold-worklist/create |
2410500 ns (± 113809) |
1806000 ns (± 84633) |
1.33 |
add-fold-worklist/rewrite |
3841500 ns (± 90991) |
3534000 ns (± 29203) |
1.09 |
add-fold-worklist-local/create |
2453000 ns (± 111449) |
1826000 ns (± 90007) |
1.34 |
add-fold-worklist-local/rewrite |
3638000 ns (± 98039) |
3295000 ns (± 54636) |
1.10 |
add-zero-worklist/create |
2455000 ns (± 114635) |
1845000 ns (± 78796) |
1.33 |
add-zero-worklist/rewrite |
2566000 ns (± 64780) |
2268000 ns (± 94240) |
1.13 |
add-zero-reuse-worklist/create |
1977500 ns (± 139506) |
1523000 ns (± 17544) |
1.30 |
add-zero-reuse-worklist/rewrite |
2150500 ns (± 71636) |
1874000 ns (± 48317) |
1.15 |
mul-two-worklist/create |
2362000 ns (± 118818) |
1777000 ns (± 14653) |
1.33 |
mul-two-worklist/rewrite |
5625000 ns (± 151261) |
4984000 ns (± 27725) |
1.13 |
add-fold-forwards/create |
2355500 ns (± 132956) |
1803000 ns (± 23043) |
1.31 |
add-fold-forwards/rewrite |
2971500 ns (± 87891) |
2654000 ns (± 26159) |
1.12 |
add-zero-forwards/create |
2237000 ns (± 44930) |
1792000 ns (± 82130) |
1.25 |
add-zero-forwards/rewrite |
1865000 ns (± 62926) |
1714000 ns (± 16956) |
1.09 |
add-zero-reuse-forwards/create |
1931000 ns (± 89164) |
1517000 ns (± 17421) |
1.27 |
add-zero-reuse-forwards/rewrite |
1543500 ns (± 38393) |
1374000 ns (± 7036) |
1.12 |
mul-two-forwards/create |
2358000 ns (± 62173) |
1810000 ns (± 91828) |
1.30 |
mul-two-forwards/rewrite |
3625000 ns (± 60156) |
3223000 ns (± 112383) |
1.12 |
add-zero-reuse-first/create |
1981000 ns (± 97207) |
1539500 ns (± 46488) |
1.29 |
add-zero-reuse-first/rewrite |
8000 ns (± 0) |
9000 ns (± 1762) |
0.89 |
add-zero-lots-of-reuse-first/create |
2016500 ns (± 117174) |
1534000 ns (± 10498) |
1.31 |
add-zero-lots-of-reuse-first/rewrite |
805500 ns (± 53344) |
783000 ns (± 20700) |
1.03 |
This comment was automatically generated by workflow using github-action-benchmark.
Introduce per-dialect `Llvm.interpretOp'_monotone` and `Riscv.interpretOp'_monotone` lemmas, and dispatch `interpretOp'_monotone` to them for the `riscv` and `llvm` cases. `Riscv.interpretOp'_monotone` is proven for `add` and `sub`; the remaining cases are still `sorry`.
tobiasgrosser
force-pushed
the
tobias/interpretOp_monotone
branch
from
July 12, 2026 07:42
4d4fe47 to
4cbe686
Compare
Add two helper lemmas: reflexivity of the interpretation-result refinement relation, and the fact that an operand array of registers is refined only by itself (registers carry no poison, so refinement on them is equality). Together they discharge `Riscv.interpretOp'_monotone` for all 110 riscv opcodes at once: either every operand is a register, and then the refined operands are the original ones, so both sides interpret to the very same result; or some operand is not a register, and every opcode that reads its operands fails to interpret, while the opcodes that ignore their operands again produce the very same result on both sides. This replaces the two hand-written `add` and `sub` cases.
`llvm.store` is not monotone for a refinement relation that requires the resulting memories to be *equal*: storing a poison value empoisons the target bytes, while storing the concrete value that refines it writes those bytes and clears their poison mask. Both stores succeed, but the two memories differ. Exclude it by hypothesis, and thread the hypothesis through `interpretOp_monotone`, `interpretOpList_mono` and `interpretTerminatedOpList_mono`. Proving `llvm.store` monotone would require relating the resulting memories by `MemoryState.isRefinedBy` rather than by equality.
…ects `builtin.unrealized_conversion_cast` from an integer to a register is, like `llvm.store`, genuinely not monotone: it maps poison to the register `0` (`LLVM.Int.toReg`), while the concrete value that refines poison maps to a different register, and refinement on registers is equality. Exclude it by hypothesis as well, and thread the hypothesis through the `Monotonicity` lemmas. With both offenders excluded, prove the `rv64`, `riscv_stack` and `hw` cases (they ignore their operands, so both sides interpret to the very same result), the `func` case (`func.return` hands its operands to the `return` action, which refines pointwise) and the remaining `builtin` opcodes (which do not interpret). Still `sorry`: the `llvm`, `arith`, `cf`, `riscv_cf` and `comb` dialects.
Destructuring of refined one- and two-element operand arrays, and refinement preservation for `Array.extract` and `getElem?`. These are the building blocks for the monotonicity proofs of the remaining dialects.
Add a lifting lemma for the dialects that do not touch memory (their result is a `(values, action)` pair that `interpretOp'` threads the unchanged memory through), and use it to discharge the `arith` case from `Arith.interpretOp'_monotone`.
`#print axioms bitcast_local_preservesSemantics` pins the names of the axioms `bv_decide` generates, and their indices shift when declarations are added to a module that `LowerBitcast` transitively imports. Only the indices change: the same axioms, in the same number, are still used.
… comb dialects None of the three touches memory, so they are lifted through `interpretResult_isRefinedBy_of_memFree`. No opcode had to be excluded: * `cf.br` and `riscv_cf.branch` hand their operands straight to a `branch` action, which refines because the operands do; * `cf.cond_br` is undefined behaviour on a poison condition (and UB is refined by anything), while a concrete condition is refined only by itself, so both sides take the same branch and pass it refining `Array.extract` slices; * the `riscv_cf` comparisons branch on registers, which carry no poison and so refine only themselves, so both sides compare the very same values; * `comb.add` is poison as soon as one argument is, and otherwise every argument is concrete and the refining ones are the very same. `Data.Comb.add` had no monotonicity lemma, so prove one.
Prove monotonicity of the `llvm` dialect interpreter, which completes `interpretOp'_monotone`: the theorem no longer depends on `sorryAx`. This needs data-level monotonicity for the operations the dialect interprets. The `Data.LLVM.Int` intrinsics (funnel shifts, count/reverse bits, min/max, abs and the saturating arithmetic) and, newly, `Data.LLVM.Byte` (`shl`, `lshr`, `trunc`) had no monotonicity lemmas, so prove them. The `nuw`/`exact` no-wrap checks are the interesting part: when the source passes them the bits shifted out are concrete zeros, so the refining target passes them too. Two further opcodes turn out to be genuinely *not* monotone, for the same reason as `llvm.store` -- they materialise poison into a representation that cannot hold it -- and are excluded by hypothesis: * `llvm.freeze` freezes poison to a concrete value (`Int.freeze poison = 0`), while the concrete value that refines poison freezes to itself, and a concrete value is refined only by itself: `#[.int 8 poison] ⊒ #[.int 8 1]`, but the source yields `0` and the target `1`. * `llvm.bitcast` from a byte to a pointer goes through `Byte.toUInt64`, which maps any poisoned byte to `0`, and addresses carry no poison, so refinement on them is equality: `#[.byte 64 allPoison] ⊒ #[.byte 64 1]` yields `.addr 0` and `.addr 1`.
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
1 participant
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.