Skip to content

Conversation

@Roy-Certora
Copy link

No description provided.

Copy link
Contributor

@nd-certora nd-certora left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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);
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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()) {
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

this is nice and I just learned a few days ago about 'selector' in call hooks

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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;
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

do we have executingContract in this point? otherwise require ed.msg.sender == currentContract; can be a wrong assumptions

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

That's true (even though here it's the only option currentContract = executingContract).
Do we have a keyword then?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants