erc721-safeTransferFrom-spec.ini

; ERC721-EVM Specification Template Parameters

[root]
k: #execute => #halt
schedule: CONSTANTINOPLE
gas: #gas(INITGAS, 0, 0) => _

[safeTransferFrom]
callData: #abiCallData("safeTransferFrom", #address(FROM_ID), #address(TO_ID), #uint256(TOKEN_ID))
refund: _ => _
requires:
    andBool 0 <=Int FROM_ID  andBool FROM_ID  <Int (2 ^Int 160)
    andBool 0 <=Int TO_ID    andBool TO_ID    <Int (2 ^Int 160)
    andBool 0 <=Int TOKEN_ID andBool TOKEN_ID <Int (2 ^Int 256)
    andBool select(M1, #hashedLocation({COMPILER}, {_IDTOOWNER},           TOKEN_ID))              ==Int  TOKEN_OWNER
    andBool select(M1, #hashedLocation({COMPILER}, {_IDTOAPPROVAL},        TOKEN_ID))              ==Int  APPROVER
    andBool select(M1, #hashedLocation({COMPILER}, {_OWNERTOOPERATORS},    TOKEN_OWNER CALLER_ID)) ==Int  OPERATOR
    andBool 0 <=Int TOKEN_OWNER andBool TOKEN_OWNER <Int (2 ^Int 160)
    andBool 0 <=Int APPROVER andBool APPROVER <Int (2 ^Int 160)
    andBool 0 <=Int OPERATOR andBool OPERATOR <Int 2

[safeTransferFrom-success]
statusCode: _ => EVMC_SUCCESS
output: _ => _
log: _:List ( .List => ListItem(#abiEventLog(ACCT_ID, "Transfer", #indexed(#address(FROM_ID)), #indexed(#address(TO_ID)), #indexed(#uint256(TOKEN_ID)))))
+requires:
    andBool ( CALLER_ID             ==Int  TOKEN_OWNER
        orBool APPROVER             ==Int  CALLER_ID
        orBool OPERATOR             ==Int  1 )
    andBool FROM_ID                 ==Int  TOKEN_OWNER
    andBool TO_ID                   =/=Int 0
    andBool TOKEN_OWNER             =/=Int 0


[safeTransferFrom-success-1]
storage: M1 => M2
origStorage: M1
+requires:
    andBool select(M1, #hashedLocation({COMPILER}, {_OWNERTONFTOKENCOUNT}, FROM_ID))               ==Int  FROM_TOKEN_COUNT
    andBool select(M1, #hashedLocation({COMPILER}, {_OWNERTONFTOKENCOUNT}, TO_ID))                 ==Int  TO_TOKEN_COUNT
    andBool 0 <=Int FROM_TOKEN_COUNT andBool FROM_TOKEN_COUNT <Int (2 ^Int 256)
    andBool 0 <=Int TO_TOKEN_COUNT andBool TO_TOKEN_COUNT <Int (2 ^Int 256)
    andBool FROM_ID =/=Int TO_ID
    andBool TO_TOKEN_COUNT +Int 1  <Int (2 ^Int 256)
    andBool FROM_TOKEN_COUNT -Int 1 >=Int 0
ensures:
    ensures select(M2, #hashedLocation({COMPILER}, {_OWNERTONFTOKENCOUNT}, FROM_ID))  ==Int FROM_TOKEN_COUNT -Int 1
    andBool select(M2, #hashedLocation({COMPILER}, {_OWNERTONFTOKENCOUNT}, TO_ID))    ==Int TO_TOKEN_COUNT   +Int 1
    ; Those 2 next lines make it fail
;    andBool select(M2, #hashedLocation({COMPILER}, {_IDTOOWNER},           TOKEN_ID)) ==Int TO_ID
;    andBool select(M2, #hashedLocation({COMPILER}, {_IDTOAPPROVAL},        TOKEN_ID)) ==Int 0
    andBool M1 ==IMap M2 except
      (SetItem(#hashedLocation({COMPILER}, {_OWNERTONFTOKENCOUNT}, FROM_ID))
       SetItem(#hashedLocation({COMPILER}, {_OWNERTONFTOKENCOUNT}, TO_ID))
       SetItem(#hashedLocation({COMPILER}, {_IDTOOWNER},           TOKEN_ID))
       SetItem(#hashedLocation({COMPILER}, {_IDTOAPPROVAL},        TOKEN_ID)) .Set)
;TODO: check if to is a smart contract and that the returned value is the correct one

; FIX ME : I'm not working
[safeTransferFrom-success-2]
storage: M1 => M2
origStorage: M1
+requires:
    andBool FROM_ID ==Int TO_ID
ensures:
    andBool select(M2, #hashedLocation({COMPILER}, {_IDTOOWNER},           TOKEN_ID)) ==Int TOKEN_OWNER
    andBool select(M2, #hashedLocation({COMPILER}, {_IDTOAPPROVAL},        TOKEN_ID)) ==Int 0
    andBool M1 ==IMap M2 except
       (SetItem(#hashedLocation({COMPILER}, {_IDTOOWNER},           TOKEN_ID))
       SetItem(#hashedLocation({COMPILER}, {_IDTOAPPROVAL},        TOKEN_ID)) .Set)

; TODO : complete with failure cases

[pgm]
compiler: "Solidity"
_idToOwner: 0
_idToApproval: 1
_ownerToNFTokenCount: 2
_ownerToOperators: 3
code: "0x608060405260043610610041576000357c0100000000000000000000000000000000000000000000000000000000900463ffffffff16806342842e0e14610046575b600080fd5b34801561005257600080fd5b506100b1600480360381019080803573ffffffffffffffffffffffffffffffffffffffff169060200190929190803573ffffffffffffffffffffffffffffffffffffffff169060200190929190803590602001909291905050506100b3565b005b6100cf83838360206040519081016040528060008152506100d4565b505050565b600080600084815260200190815260200160002060009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1690503373ffffffffffffffffffffffffffffffffffffffff168173ffffffffffffffffffffffffffffffffffffffff1614806101a357503373ffffffffffffffffffffffffffffffffffffffff166001600085815260200190815260200160002060009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16145b806102345750600360008273ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060009054906101000a900460ff165b151561023f57600080fd5b600073ffffffffffffffffffffffffffffffffffffffff1660008085815260200190815260200160002060009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16141515156102ad57600080fd5b8473ffffffffffffffffffffffffffffffffffffffff168173ffffffffffffffffffffffffffffffffffffffff161415156102e757600080fd5b600073ffffffffffffffffffffffffffffffffffffffff168473ffffffffffffffffffffffffffffffffffffffff161415151561032357600080fd5b61032d8484610334565b5050505050565b600080600083815260200190815260200160002060009054906101000a900473ffffffffffffffffffffffffffffffffffffffff169050610374826103e8565b61037e8183610475565b61038883836105eb565b818373ffffffffffffffffffffffffffffffffffffffff168273ffffffffffffffffffffffffffffffffffffffff167fddf252ad1be2c89b69c2b068fc378daa952ba7f163c4a11628f55a4df523b3ef60405160405180910390a4505050565b60006001600083815260200190815260200160002060009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16141515610472576001600082815260200190815260200160002060006101000a81549073ffffffffffffffffffffffffffffffffffffffff02191690555b50565b8173ffffffffffffffffffffffffffffffffffffffff1660008083815260200190815260200160002060009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff161415156104e157600080fd5b6000600260008473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000205411151561052c57fe5b6001600260008473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000205403600260008473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000208190555060008082815260200190815260200160002060006101000a81549073ffffffffffffffffffffffffffffffffffffffff02191690555050565b60008073ffffffffffffffffffffffffffffffffffffffff1660008084815260200190815260200160002060009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1614151561065957600080fd5b8260008084815260200190815260200160002060006101000a81548173ffffffffffffffffffffffffffffffffffffffff021916908373ffffffffffffffffffffffffffffffffffffffff160217905550600260008473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002054905060018101600260008573ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000208190555080600260008573ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020541015151561078157600080fd5b5050505600a165627a7a723058200916b370029892fcaa547bb48c2f21b851ceda6b506210122db8508cb88d6f8d0029"

erc721-safeTransferFrom-spec.sol

pragma solidity ^0.4.24;

/**
 * @dev Implementation of ERC-721 non-fungible token standard.
 * From 0xcert
 */
contract NFToken
{
  mapping (uint256 => address) internal idToOwner;
  mapping (uint256 => address) internal idToApprovals;
  mapping (address => uint256) private ownerToNFTokenCount;
  mapping (address => mapping (address => bool)) internal ownerToOperators;

  constructor()
    public
  {

  }

  event Transfer(
    address indexed _from,
    address indexed _to,
    uint256 indexed _tokenId
  );

  function safeTransferFrom(
    address _from,
    address _to,
    uint256 _tokenId
  )
    external
  {
    _safeTransferFrom(_from, _to, _tokenId, "");
  }

    function _safeTransferFrom(
    address _from,
    address _to,
    uint256 _tokenId,
    bytes _data
  )
    private
  {
    address tokenOwner = idToOwner[_tokenId];
    require(
      tokenOwner == msg.sender
      || idToApprovals[_tokenId] == msg.sender
      || ownerToOperators[tokenOwner][msg.sender]
    );
    require(idToOwner[_tokenId] != address(0));

    require(tokenOwner == _from);
    require(_to != address(0));

    _transfer(_to, _tokenId);

    /*if (_to.isContract()) {
      bytes4 retval = ERC721TokenReceiver(_to).onERC721Received(msg.sender, _from, _tokenId, _data);
      require(retval == MAGIC_ON_ERC721_RECEIVED);
    }*/
  }

  function _transfer(
    address _to,
    uint256 _tokenId
  )
    internal
  {
    address from = idToOwner[_tokenId];
    clearApproval(_tokenId);

    removeNFToken(from, _tokenId);
    addNFToken(_to, _tokenId);

    emit Transfer(from, _to, _tokenId);
  }
  
  function clearApproval(
    uint256 _tokenId
  )
    private
  {
    if(idToApprovals[_tokenId] != 0)
    {
      delete idToApprovals[_tokenId];
    }
  }

  function removeNFToken(
    address _from,
    uint256 _tokenId
  )
   internal
  {
    require(idToOwner[_tokenId] == _from);
    assert(ownerToNFTokenCount[_from] > 0);
    ownerToNFTokenCount[_from] = ownerToNFTokenCount[_from] - 1;
    delete idToOwner[_tokenId];
  }

  function addNFToken(
    address _to,
    uint256 _tokenId
  )
    internal
  {
    require(idToOwner[_tokenId] == address(0));

    idToOwner[_tokenId] = _to;
    uint256 oldVal = ownerToNFTokenCount[_to];
    ownerToNFTokenCount[_to] = oldVal + 1;
    require(ownerToNFTokenCount[_to] >= oldVal);
  }
}