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.
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
Deposit contract fixes #1362
Deposit contract fixes #1362
Changes from all commits
39278b3
891524f
f6ec278
08d32a8
7950ef0
162c30d
caa566f
17740c3
9cfde12
62629c9
File filter
Filter by extension
Conversations
Jump to
There are no files selected for viewing
Large diffs are not rendered by default.
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.
We should add these length checks back in until/unless formal verification shows safe to remove
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.
cc @daejunpark :)
(As a side note, I expect the
deposit_data_root
check to catch everything. If there's anything funny going on when Merkleising the deposit data then there's cryptographically no way the deposit contract will get a matchingdeposit_data_root
.)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.
^ That suggestion was made after talking directly with @daejunpark last week
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.
@JustinDrake I found that the new Vyper compiler made some nontrivial changes to the bytecode, so keeping the length check for now will make it easier for us to re-run the formal verification, focusing on ensuring that both the Vyper compiler update and the checksum change work as expected. Then, a separate PR can be made that removes the length check, once we re-run the verification again on the code without the length check. Does that work for you?
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.
Yep, makes sense :) I've readded the length checks and recompiled—we can reassess after verification has been re-run.
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.
@JustinDrake Could you please elaborate what you mean by "the sha256 function respecting the len"?
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.
I mean that if
y = sha256(x, len=l)
then the outputy
has a corresponding preimage with length exactlyl
.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.
@JustinDrake I guess you mean
sha256(slice(x, start=0, len=1))
, right? In that case, yes,sha256
takes only the sliced range, and our formal verification result confirmed that the compiled bytecode agrees on that in the presence of the length check. (We will need additional formal verification to confirm the same thing without the length check, though.)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.
So, how should we proceed here?
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.
I'm in favor of keeping the length check. It is easier to reason about and keeps the existing work in place.