-
Notifications
You must be signed in to change notification settings - Fork 121
[WIP] Optimistic Precompiles #3443
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
base: collect-empirical-constraints
Are you sure you want to change the base?
Changes from all commits
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -187,6 +187,20 @@ fn redundant_memory_interactions_indices< | |
| // In that case, we can replace both bus interactions with equality constraints | ||
| // between the data that would have been sent and received. | ||
| if let Some((previous_send, existing_values)) = memory_contents.remove(&addr) { | ||
| // TODO: This can happen which optimistic precompiles, because basic block can include | ||
| // big-word branching instructions. This hot fix is NOT sounds, because it does not handle | ||
| // a situation where we write a (small-word) limb, accesses the large word, and then the | ||
| // small-word limb again. | ||
| if existing_values.len() != mem_int.data().len() { | ||
| log::error!( | ||
| "Memory interaction data length mismatch: existing values = {}, new values = {}. Resetting memory.", | ||
| existing_values.iter().map(ToString::to_string).join(", "), | ||
| mem_int.data().iter().map(ToString::to_string).join(", ") | ||
| ); | ||
| memory_contents.clear(); | ||
| continue; | ||
| } | ||
|
Comment on lines
+194
to
+202
Collaborator
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Why is this needed here?
Collaborator
Author
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. This appears because some of OpenVM's 256-Bit branch instructions can appear in a basic block. These instruction read larger words. I think we should fix this by not including these instructions inside a basic block, like we do for other precompiles (= non RISC-V instructions). Doing this properly would really complicate the memory optimizer and I don't think it's worth it. |
||
|
|
||
| for (existing, new) in existing_values.iter().zip_eq(mem_int.data().iter()) { | ||
| new_constraints.push(AlgebraicConstraint::assert_zero( | ||
| existing.clone() - new.clone(), | ||
|
|
||
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This should be fixed before merging. I suggest to black-list big-word instructions.