feat(rewriter): RAUW + erase is safe#936
Draft
regehr wants to merge 3 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: 067636a | Previous: a8086a5 | Ratio |
|---|---|---|---|
add-fold-worklist/create |
2024000 ns (± 66017) |
2191000 ns (± 116585) |
0.92 |
add-fold-worklist/rewrite |
3196000 ns (± 34674) |
4025500 ns (± 99281) |
0.79 |
add-fold-worklist-local/create |
2003000 ns (± 52099) |
2104000 ns (± 59879) |
0.95 |
add-fold-worklist-local/rewrite |
2764000 ns (± 23755) |
3305000 ns (± 90508) |
0.84 |
add-zero-worklist/create |
2019000 ns (± 46483) |
2234000 ns (± 109081) |
0.90 |
add-zero-worklist/rewrite |
2153000 ns (± 13838) |
2750000 ns (± 105299) |
0.78 |
add-zero-reuse-worklist/create |
1580000 ns (± 49617) |
1842000 ns (± 83972) |
0.86 |
add-zero-reuse-worklist/rewrite |
1836000 ns (± 18349) |
2160000 ns (± 52555) |
0.85 |
mul-two-worklist/create |
1959000 ns (± 48397) |
2231000 ns (± 55895) |
0.88 |
mul-two-worklist/rewrite |
4632000 ns (± 19857) |
5644500 ns (± 283151) |
0.82 |
add-fold-forwards/create |
2029000 ns (± 23921) |
2202000 ns (± 109662) |
0.92 |
add-fold-forwards/rewrite |
2531000 ns (± 19540) |
3032000 ns (± 65213) |
0.83 |
add-zero-forwards/create |
1950000 ns (± 29636) |
2265000 ns (± 96205) |
0.86 |
add-zero-forwards/rewrite |
1692000 ns (± 28244) |
1987500 ns (± 93854) |
0.85 |
add-zero-reuse-forwards/create |
1651000 ns (± 30830) |
1832000 ns (± 89057) |
0.90 |
add-zero-reuse-forwards/rewrite |
1413000 ns (± 34759) |
1542000 ns (± 22638) |
0.92 |
mul-two-forwards/create |
2048000 ns (± 65757) |
2198000 ns (± 41455) |
0.93 |
mul-two-forwards/rewrite |
3034000 ns (± 16392) |
3767000 ns (± 172147) |
0.81 |
add-zero-reuse-first/create |
1640000 ns (± 42305) |
1855500 ns (± 114257) |
0.88 |
add-zero-reuse-first/rewrite |
11000 ns (± 0) |
8500 ns (± 2543) |
1.29 |
add-zero-lots-of-reuse-first/create |
1588000 ns (± 36219) |
1789000 ns (± 89329) |
0.89 |
add-zero-lots-of-reuse-first/rewrite |
717000 ns (± 31076) |
803000 ns (± 57817) |
0.89 |
This comment was automatically generated by workflow using github-action-benchmark.
math-fehr
reviewed
Jun 29, 2026
math-fehr
left a comment
math-fehr
left a comment
Collaborator
There was a problem hiding this comment.
Thanks! I left some comments, but otherwise I feel that's going to be quite useful.
also, as I mentionned in the comments, I feel we should just fix eraseOp!
Comment on lines
+218
to
+239
| @[simp, grind =] | ||
| theorem replaceValue_ctx {rewriter : PatternRewriter OpInfo} {oldVal newVal : ValuePtr} | ||
| {neValues : oldVal ≠ newVal} {oldIn : oldVal.InBounds rewriter.ctx.raw} | ||
| {newIn : newVal.InBounds rewriter.ctx.raw} : | ||
| (rewriter.replaceValue oldVal newVal neValues oldIn newIn).ctx | ||
| = WfRewriter.replaceValue rewriter.ctx oldVal newVal neValues oldIn newIn := by | ||
| simp [replaceValue, addUsersInWorklist_same_ctx] | ||
|
|
||
| /-- After replacing `op`'s single result with `newValue`, erasing `op` succeeds: the three | ||
| preconditions of `eraseOp` (`op` in bounds, no regions, no uses) hold in the resulting rewriter. -/ | ||
| theorem eraseOp_some_after_replace_result0 | ||
| (rewriter : PatternRewriter OpInfo) (op : OperationPtr) (newValue : ValuePtr) | ||
| (hop : op.InBounds rewriter.ctx.raw) | ||
| (hres : (op.getResult 0 : ValuePtr).InBounds rewriter.ctx.raw) | ||
| (hnew : newValue.InBounds rewriter.ctx.raw) | ||
| (hne : (op.getResult 0 : ValuePtr) ≠ newValue) | ||
| (hone : op.getNumResults! rewriter.ctx.raw = 1) | ||
| (hregions : op.getNumRegions! rewriter.ctx.raw = 0) : | ||
| ∃ rewriter', | ||
| (rewriter.replaceValue (op.getResult 0 : ValuePtr) newValue hne hres hnew).eraseOp op | ||
| = some rewriter' := | ||
| ⟨_, rfl⟩ |
Collaborator
There was a problem hiding this comment.
Can you move these lemmas to a new file PatternRewriter/Lemmas.lean (unless one exist already?)
Comment on lines
+228
to
+239
| theorem eraseOp_some_after_replace_result0 | ||
| (rewriter : PatternRewriter OpInfo) (op : OperationPtr) (newValue : ValuePtr) | ||
| (hop : op.InBounds rewriter.ctx.raw) | ||
| (hres : (op.getResult 0 : ValuePtr).InBounds rewriter.ctx.raw) | ||
| (hnew : newValue.InBounds rewriter.ctx.raw) | ||
| (hne : (op.getResult 0 : ValuePtr) ≠ newValue) | ||
| (hone : op.getNumResults! rewriter.ctx.raw = 1) | ||
| (hregions : op.getNumRegions! rewriter.ctx.raw = 0) : | ||
| ∃ rewriter', | ||
| (rewriter.replaceValue (op.getResult 0 : ValuePtr) newValue hne hres hnew).eraseOp op | ||
| = some rewriter' := | ||
| ⟨_, rfl⟩ |
Collaborator
There was a problem hiding this comment.
Well, I realize from your theorem that my definition of eraseOp returned an option for no reasons ^^'
eraseOp should always succeed, and your proof is essentially not even using your hypotheses to be proven.
I think we should then rather have a PR that removes the Option from eraseOp here, and that should make things easier!
Comment on lines
+888
to
+891
| {op : OperationPtr} {newValue : ValuePtr} | ||
| {hres : (op.getResult 0 : ValuePtr).InBounds ctx.raw} | ||
| {hnew : newValue.InBounds ctx.raw} | ||
| {hne : (op.getResult 0 : ValuePtr) ≠ newValue} |
Collaborator
There was a problem hiding this comment.
I believe you can just remove these parameters, as they can be inferred from the goal. That should make this a bit nicer to read
Comment on lines
+906
to
+918
| theorem OperationPtr.erase_preconditions_after_replace_result0 | ||
| {op : OperationPtr} {newValue : ValuePtr} | ||
| (hop : op.InBounds ctx.raw) | ||
| (hres : (op.getResult 0 : ValuePtr).InBounds ctx.raw) | ||
| (hnew : newValue.InBounds ctx.raw) | ||
| (hne : (op.getResult 0 : ValuePtr) ≠ newValue) | ||
| (hone : op.getNumResults! ctx.raw = 1) | ||
| (hregions : op.getNumRegions! ctx.raw = 0) : | ||
| let ctx' := | ||
| WfRewriter.replaceValue ctx (op.getResult 0 : ValuePtr) newValue hne hres hnew | ||
| op.InBounds ctx'.raw ∧ | ||
| op.getNumRegions! ctx'.raw = 0 ∧ | ||
| op.hasUses! ctx'.raw = false := by |
Collaborator
There was a problem hiding this comment.
I'm not sure we overall need this theorem?
Mostly because each component is already a simp/grind lemma?
| have hidx0 : index = 0 := by omega | ||
| subst hidx0 | ||
| exact ValuePtr.hasUses!_WfRewriter_replaceValue_oldValue | ||
|
|
Collaborator
There was a problem hiding this comment.
Can you add these to a new Rewriter/WfRewriter/Lemmas.lean?
I'm trying to have GetSet.lean being very mechanical, and this is slightly outside of its scope!
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.
Mathieu if you have time to give me feedback on this I would appreciate it.
I was going to do more work on Verifier.lean but it seems like maybe starting here is more useful, and then I can go back to the verifier lemmas once I know more about what exactly they must provide