feat(interpret): prove interpretOp' monotone for the riscv dialect#1069
Open
tobiasgrosser wants to merge 3 commits into
Open
feat(interpret): prove interpretOp' monotone for the riscv dialect#1069tobiasgrosser wants to merge 3 commits into
interpretOp' monotone for the riscv dialect#1069tobiasgrosser wants to merge 3 commits into
Conversation
RISC-V operands are registers, which carry no poison, so refinement on them is equality: an operand array of registers is refined only by itself (`RuntimeValue.eq_of_arrayIsRefinedBy_of_regs`). That discharges all 110 riscv opcodes at once, without reasoning about any of them individually: 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 (`li`, `lui`) again produce the very same result on both sides. Dispatch the `riscv` case of `interpretOp'_monotone` to it. The other dialects remain `sorry`.
![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: 107ad9e | Previous: 14ba44d | Ratio |
|---|---|---|---|
add-fold-worklist/create |
2307000 ns (± 93271) |
1772000 ns (± 84750) |
1.30 |
add-fold-worklist/rewrite |
3910000 ns (± 57578) |
2742000 ns (± 36738) |
1.43 |
add-fold-worklist-local/create |
2497000 ns (± 46869) |
1627000 ns (± 67114) |
1.53 |
add-fold-worklist-local/rewrite |
3740000 ns (± 78764) |
2665000 ns (± 22917) |
1.40 |
add-zero-worklist/create |
2398000 ns (± 75758) |
1789000 ns (± 69121) |
1.34 |
add-zero-worklist/rewrite |
2556000 ns (± 98889) |
1870000 ns (± 45602) |
1.37 |
add-zero-reuse-worklist/create |
2023500 ns (± 140907) |
1447000 ns (± 72595) |
1.40 |
add-zero-reuse-worklist/rewrite |
2098000 ns (± 69960) |
1684000 ns (± 84371) |
1.25 |
mul-two-worklist/create |
2401000 ns (± 121389) |
1681000 ns (± 118759) |
1.43 |
mul-two-worklist/rewrite |
5643000 ns (± 125731) |
4044500 ns (± 157988) |
1.40 |
add-fold-forwards/create |
2253000 ns (± 127901) |
1802000 ns (± 15991) |
1.25 |
add-fold-forwards/rewrite |
2999500 ns (± 53197) |
2244000 ns (± 34158) |
1.34 |
add-zero-forwards/create |
2302500 ns (± 114364) |
1795000 ns (± 85264) |
1.28 |
add-zero-forwards/rewrite |
1920500 ns (± 66705) |
1477000 ns (± 57928) |
1.30 |
add-zero-reuse-forwards/create |
1921000 ns (± 32965) |
1425500 ns (± 89350) |
1.35 |
add-zero-reuse-forwards/rewrite |
1587000 ns (± 60069) |
1207000 ns (± 51940) |
1.31 |
mul-two-forwards/create |
2307000 ns (± 96500) |
1749500 ns (± 136270) |
1.32 |
mul-two-forwards/rewrite |
3680000 ns (± 94315) |
2652000 ns (± 123050) |
1.39 |
add-zero-reuse-first/create |
1941500 ns (± 152514) |
1353500 ns (± 97220) |
1.43 |
add-zero-reuse-first/rewrite |
9000 ns (± 2120) |
10500 ns (± 2343) |
0.86 |
add-zero-lots-of-reuse-first/create |
1970500 ns (± 147963) |
1417500 ns (± 114949) |
1.39 |
add-zero-lots-of-reuse-first/rewrite |
765500 ns (± 59457) |
632000 ns (± 54323) |
1.21 |
This comment was automatically generated by workflow using github-action-benchmark.
math-fehr
reviewed
Jul 12, 2026
math-fehr
left a comment
math-fehr
left a comment
Collaborator
There was a problem hiding this comment.
I had a few comments on the proof strategy, but nice otherwise!
Comment on lines
+521
to
+525
| abbrev InterpretResultIsRefinedBy : | ||
| Array RuntimeValue × MemoryState × Option ControlFlowAction → | ||
| Array RuntimeValue × MemoryState × Option ControlFlowAction → Prop := | ||
| fun r₁ r₂ => r₁.1 ⊒ r₂.1 ∧ r₁.2.1 = r₂.2.1 ∧ | ||
| ControlFlowAction.optionIsRefinedBy r₁.2.2 r₂.2.2 |
Collaborator
There was a problem hiding this comment.
This should probably be added in Interpreter/Basic.lean if possible. Unless there is a cycle of dependency from that?
In any case, since this is introduced, we should also use it in the other parts of the codebase I would say.
math-fehr
approved these changes
Jul 12, 2026
math-fehr
left a comment
math-fehr
left a comment
Collaborator
There was a problem hiding this comment.
Just one comment on some documentation, but otherwise all good!
| A RISC-V operation that interprets successfully produces register results and no control flow | ||
| action: a single register for the arithmetic and load opcodes, and no result at all for the stores. | ||
| Note that the memory is *not* preserved -- loads grow it via `ensureSize` and stores write to it. | ||
| -/ |
Collaborator
There was a problem hiding this comment.
Suggested change
| -/ | |
| action: a single register for the arithmetic and load opcodes, and no result at all for the stores. |
I am not sure why mentioning memory preservation here?
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.
RISC-V operands are registers, which carry no poison, so refinement on them is
equality: an operand array of registers is refined only by itself
(
RuntimeValue.eq_of_arrayIsRefinedBy_of_regs). That discharges all 110 riscvopcodes at once, without reasoning about any of them individually: 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 (
li,lui) again produce the very same result onboth sides.
Dispatch the
riscvcase ofinterpretOp'_monotoneto it. The other dialectsremain
sorry.