Multiple contracts, with a contract that is not created

[jaa2]

Is it possible to define variables representing addresses contracts with known interfaces which aren't created by the contract referring to them?

For example, could you write an act specification for this?

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.0;

interface IERC20 {
    function transfer(address recipient, uint256 amount) external;
}

contract TransferOneToken {
    IERC20 public token;

    constructor(IERC20 _tokenAddress) {
        require(address(_tokenAddress) != address(0), "Invalid token address");
        token = _tokenAddress;
    }

    function transfer() public {
        // Transfer 1 token from the contract to the sender
        uint256 transferAmt = 1;
        token.transfer(msg.sender, transferAmt);
    }
}

[zoep]

Hi @jaa2 ! Thanks so much for your interest in Act! I'm quoting the answers to the same thread in Element.

@d-xo :

we're very close to a finished implementation for this
the casting branch has a working version that will let you cast addresses to contracts like this: https://github.com/ethereum/act/blob/0ac36b486492b82d4193514611aab85a465ae6c1/tests/hevm/pass/cast-2/cast.act#L71
it gets pretty intense soundness wise when you start to consider all the potential for aliasing that this feature introduces though
so there's still some thought and work required to make it safe

@zoep :

As dxo mentioned supporting casting from addresses to contracts is currently underway. In the general cases, it can get very complicated as there are issues with aliasing. However, simple cases like the one you wrote in the issue are supported.
Here is a modified version of the code you wrote and the corresponding act spec. The two can be proved equivalent.

Solidity:

pragma solidity ^0.8.0;

contract Token {
  mapping (address => uint) public balanceOf;

  constructor(uint _totalSupply) {
      balanceOf[msg.sender] = _totalSupply;
  }


  function transfer(address to, uint256 value) public returns (uint) {
  balanceOf[msg.sender] = balanceOf[msg.sender] - value;
      balanceOf[to] = balanceOf[to] + value;
      return 1;
  }
  
}

contract TransferOneToken {
  Token token;

  constructor(address _tokenAddress) {
      require(_tokenAddress != address(0), "Invalid token address");
      token = Token(_tokenAddress);
  }

  function transfer() public returns (uint) {
      // Transfer 1 token from the contract to the sender
      uint256 transferAmt = 1;
      token.transfer(msg.sender, transferAmt);
  return 1;
  }
}

Act:

behaviour transfer of Token
interface transfer(address to, uint256 value)

iff

  CALLVALUE == 0
  CALLER =/= to => inRange(uint256, balanceOf[to] + value)
  inRange(uint256,balanceOf[CALLER] - value)

case CALLER =/= to:

  storage

    balanceOf[CALLER]  => balanceOf[CALLER] - value
    balanceOf[to]    => balanceOf[to] + value

  returns 1

case CALLER == to:

  returns 1


constructor of TransferOneToken
interface constructor(address _tokenAddress)

iff

    CALLVALUE == 0
    _tokenAddress =/= 0

creates

    Token token := _tokenAddress as Token

behaviour transfer of TransferOneToken
interface transfer()

iff
    CALLVALUE == 0    
    THIS =/= CALLER => inRange(uint256, token.balanceOf[CALLER] + 1)
    inRange(uint256,token.balanceOf[THIS] - 1)

case CALLER =/= THIS:

storage

    token.balanceOf[CALLER] => token.balanceOf[CALLER] + 1
    token.balanceOf[THIS]  => token.balanceOf[THIS] - 1

returns 1

case CALLER == THIS:

returns 1

Notes:

• Since we don't support interfaces (at least yet), the Token contract must be inlined (we do not support imports from other files -- at least yet).
• To make the above work, I added a return value to the transfer function of the TransferOneToken contract, but this is for a rather superficial reason. Currently in Act we do not have surface syntax for denoting no change in storage and no return value (the case CALLER == THIS would have to be empty, but this is not valid syntax). I expect this to be fixed soon.

I hope this helps! As we are working towards making Act more applicable to real smart contracts we very much appreciate user feedback and requests for features