Conversation
nd-certora
left a comment
There was a problem hiding this comment.
rather big exmaple, we will smaller example that demonstrate a specific feature or how to handle something.
| function ERC20Utils.safeTransfer(address token, address recipient, uint256 amount) internal returns (bool) with (env e) => dispatchTransfer(e, token, recipient, amount); | ||
| function ERC20Utils.safeTransferFrom(address token, address sender, address recipient, uint256 amount) internal returns (bool) with (env e) => dispatchTransferFrom(e, token, sender, recipient, amount); | ||
| function ERC20Utils.approve(address token, address to) internal with (env e) => dispatchApprove(e, token, to); | ||
| function ERC20Utils.permit(address token, bytes calldata data) internal with (env e) => dispatchPermit(e, token, data); |
There was a problem hiding this comment.
I wonder if the dispatcher list option can work here, maybe is it just for unresolved calls. would it make it simple if it is allowed?
There was a problem hiding this comment.
There are two benefits for using this approach:
First, it allows us to control the arguments of the function,
Second, it removes the underlying assembly code from the flow and immediately calls the Solidity alternative.
| } | ||
|
|
||
| hook CALL(uint g, address addr, uint value, uint argsOffset, uint argsLength, uint retOffset, uint retLength) uint rc { | ||
| if (selector == transfer_sig()) { |
There was a problem hiding this comment.
this is nice and I just learned a few days ago about 'selector' in call hooks
There was a problem hiding this comment.
I see why: it's not obvious from the syntax that this keyword exists.
|
|
||
| function dispatchTransfer(env e, address token, address recipient, uint256 amount) returns bool { | ||
| env ed; /// Dispatch environment | ||
| require ed.msg.sender == currentContract; |
There was a problem hiding this comment.
do we have executingContract in this point? otherwise require ed.msg.sender == currentContract; can be a wrong assumptions
There was a problem hiding this comment.
That's true (even though here it's the only option currentContract = executingContract).
Do we have a keyword then?
No description provided.