Deposit contract fixes #1362
Deposit contract fixes #1362
Conversation
JustinDrake
added
scope:deposit contract
post-freeze (substantive)
|
@JustinDrake do you mind also updating the deposit contract spec? (https://github.com/ethereum/eth2.0-specs/blob/0e7287eda5ea7601707a5a4e2167f98fab699644/specs/core/0_deposit-contract.md#deposit-function) Otherwise, this PR looks good to me. :) |
done 👍 |
| deposit_amount: uint256 = msg.value / as_wei_value(1, "gwei") | ||
| assert deposit_amount >= MIN_DEPOSIT_AMOUNT | ||
| assert len(pubkey) == PUBKEY_LENGTH |
There was a problem hiding this comment.
We should add these length checks back in until/unless formal verification shows safe to remove
There was a problem hiding this comment.
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 matching deposit_data_root.)
There was a problem hiding this comment.
^ That suggestion was made after talking directly with @daejunpark last week
There was a problem hiding this comment.
@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.
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.
@JustinDrake Could you please elaborate what you mean by "the sha256 function respecting the len"?
There was a problem hiding this comment.
what you mean by "the sha256 function respecting the len"?
I mean that if y = sha256(x, len=l) then the output y has a corresponding preimage with length exactly l.
There was a problem hiding this comment.
@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.
So, how should we proceed here?
- Keep the length check
- Remove the length check and do additional formal verification
There was a problem hiding this comment.
I'm in favor of keeping the length check. It is easier to reason about and keeps the existing work in place.
* dev: (25 commits) Update README.md Update README.md Update sync_protocol.md Update sync_protocol.md Update sync_protocol.md Deposit contract fixes (#1362) fix minor testing bug Update specs/networking/p2p-interface.md add note on local aggregation for interop Fix ssz-generic bitvector tests: those invalid cases of higher length than type describes, but same byte size, should have at least 1 bit set in the overflow to be invalid minor formatting Minor corrections and clarifications to the network specification doc standardization for networking spec (#1338) discuss length-prefixing pro/con, consider for removal, add link cleanups Updates apply more editorial suggestions. apply editorial suggestions. fmt. document doctoc command for posterity. ...
Address #1341, #1357 and #1279.