Open
Conversation
4311770 to
b0fc03c
Compare
huitseeker
reviewed
Mar 16, 2026
Contributor
huitseeker
left a comment
There was a problem hiding this comment.
I think the duplicate-key rejection can be bypassed in batch paths, see inline.
da9c7d5 to
477f1ae
Compare
Collaborator
Author
|
Good catch on that. I had it in my head that I was sorting directly by |
This change makes it so all SMT operations that operate on batches of key-value pairs will reject any input where the same key occurs more than once. This ensures that all of the various SMT implementations are coherent on the results they provide as there are no longer order-dependent computations. This commit introduces no measurable performance change for any impacted code path. No performance regressions are included.
477f1ae to
f07e43a
Compare
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
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.
Describe your changes
This change makes it so all SMT operations that operate on batches of key-value pairs will reject any input where the same key occurs more than once. This ensures that all of the various SMT implementations are coherent on the results they provide as there are no longer order-dependent computations.
This commit introduces no measurable performance change when it comes to the concurrent and sequential
compute_mutationsversions, andLargeSmtdoes not suffer any performance regressions either.I've left
LargeSmtForestout of this PR for the simple reason that it already has its own way of handling this. Its input batchesSmtUpdateBatchandForestUpdateBatchalways deduplicate and retain the last operation for any key. Please let me know if you'd like to see the forest return an error instead. It's a fairly trivial change.Performance-wise, best I can tell this causes no regressions. I am having some strange issue with the benchmarks today where some operations will regress and others will stay the same, and then when I re-run others will regress and the prior regressions will go back to normal. If somebody reviewing this could run the following benchmarks before and after this commit to confirm my findings here I would be most appreciative.
smt.rs: smt_compute_mutations smt_apply_mutations smt_batch_updates smt_insertlarge_smt.rs: large_smt_compute_mutations large_smt_apply_mutations large_smt_insert_batch large_smt_insert_batch_to_empty_tree large_smt_insert_batch_to_populated_tree memory_smt_compute_mutations memory_smt_apply_mutations memory_smt_insert_batchCloses #867.
Checklist before requesting a review
nextaccording to naming convention.